1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Chris Hughes
  5  -/
  6  
  7  import data.int.modeq data.int.gcd data.fintype data.pnat.basic tactic.ring
src         └────────────┘ └──────────┘ └──────────┘ └─────────────┘ └─────────┘
  8  
  9  /-!
 10  # Integers mod `n`
 11  
 12  Definition of the integers mod n, and the field structure on the integers mod p.
 13  
 14  There are two types defined, `zmod n`, which is for integers modulo a positive nat `n : ℕ+`.
 15  `zmodp` is the type of integers modulo a prime number, for which a field structure is defined.
 16  
 17  ## Definitions
 18  
 19  * `val` is inherited from `fin` and returns the least natural number in the equivalence class
 20  
 21  * `val_min_abs` returns the integer closest to zero in the equivalence class.
 22  
 23  * A coercion `cast` is defined from `zmod n` into any semiring. This is a semiring hom if the ring has
 24  characteristic dividing `n`
 25  
 26  ## Implentation notes
 27  
 28  `zmod` and `zmodp` are implemented as different types so that the field instance for `zmodp` can be
 29  synthesized. This leads to a lot of code duplication and most of the functions and theorems for
 30  `zmod` are restated for `zmodp`
 31  -/
 32  
 33  open nat nat.modeq int
 34  
 35  def zmod (n : ℕ+) := fin n
id                 └┘     └─┘ 
src                └┘     └─┘
typ                └┘     └─┘ 
doc                └┘
 36  
 37  namespace zmod
 38  
 39  instance (n : ℕ+) : has_neg (zmod n) :=
id                 └┘    └─────┘  └──┘ 
src                └┘    └─────┘  └──┘
typ                └┘    └─────┘  └──┘ 
doc                └┘
 40  ⟨λ a, ⟨nat_mod (-(a.1 : ℤ)) n,
id         └─────┘          
src         └─────┘        
typ        └─────┘          
 41    have h : (n : ℤ) ≠ 0 := int.coe_nat_ne_zero_iff_pos.2 n.pos,
id                          └─────────────────────────┘  └──┘
src                          └─────────────────────────┘   └──┘
typ                         └─────────────────────────┘  └──┘
 42    have h₁ : ((n : ℕ) : ℤ) = abs n := (abs_of_nonneg (int.coe_nat_nonneg n)).symm,
id                           └─┘      └───────────┘  └────────────────┘   └──┘
src                           └─┘       └───────────┘  └────────────────┘    └──┘
typ                          └─┘      └───────────┘  └────────────────┘   └──┘
 43    by rw [← int.coe_nat_lt, nat_mod, to_nat_of_nonneg (int.mod_nonneg _ h), h₁];
id              └────────────┘  └─────┘  └──────────────┘  └────────────┘      └┘
src       └────┘└────────────┘└┘└─────┘└┘└──────────────┘ └────────────┘└─┘ └─┘  
typ       └────┘└────────────┘└┘└─────┘└┘└──────────────┘ └────────────┘└─┘└─┘└┘
doc       └────┘              └┘       └┘                               └─┘ └─┘  
txt       └────┘              └┘       └┘                               └─┘ └─┘  
par       └────┘              └┘       └┘                               └─┘ └─┘  
pid         └──┘              └┘       └┘                               └─┘ └─┘  
st       └───────────────────┘└───────┘└─────────────────────────────────────┘└──┘└─
 44      exact int.mod_lt _ h⟩⟩
id             └────────┘   
src      └────┘└────────┘└─┘
typ      └────┘└────────┘└─┘
doc      └────┘          └─┘
txt      └────┘          └─┘
par      └────┘          └─┘
pid                     └─┘
st   ───────────────────────┘
 45  
 46  instance (n : ℕ+) : add_comm_semigroup (zmod n) :=
id                 └┘    └────────────────┘  └──┘ 
src                └┘    └────────────────┘  └──┘
typ                └┘    └────────────────┘  └──┘ 
doc                └┘
 47  { add_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id                                       └───────────┘
src                                            └───────────┘
typ                                      └───────────┘
 48      (show ((a + b) % n + c) ≡ (a + (b + c) % n) [MOD n],
id                                          └──┘ 
src                                           └──┘  
typ                                         └──┘ 
doc                                                 └──┘  
 49      from calc ((a + b) % n + c) ≡ a + b + c [MOD n] : modeq_add (nat.mod_mod _ _) rfl
id                                                   └───────┘  └─────────┘      └─┘
src                                                   └───────┘  └─────────┘      └─┘
typ                                                  └───────┘  └─────────┘      └─┘
 50        ... ≡ a + (b + c) [MOD n] : by rw add_assoc
id                                         └───────┘
src                                     └─┘└───────┘
typ                                     └─┘└───────┘
doc                                       └─┘         
txt                                       └─┘         
par                                       └─┘         
pid                                                  
st                                       └─────────────
 51        ... ≡ (a + (b + c) % n) [MOD n] : modeq_add rfl (nat.mod_mod _ _).symm),
id                                       └───────┘ └─┘  └─────────┘     └──┘
src  ─────┘                               └───────┘ └─┘  └─────────┘     └──┘
typ  ─────┘                              └───────┘ └─┘  └─────────┘     └──┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘
 52    add_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a + b) % n = (b + a) % n, by rw add_comm),
id                              └───────────┘                                 └──────┘
src                                 └───────────┘                                └─┘└──────┘
typ                             └───────────┘                              └─┘└──────┘
doc                                                                                   └─┘
txt                                                                                   └─┘
par                                                                                   └─┘
pid                                                                                     
st                                                                                   └──────────┘
 53    ..fin.has_add }
id       └─────────┘
src      └─────────┘
typ      └─────────┘
 54  
 55  instance (n : ℕ+) : comm_semigroup (zmod n) :=
id                 └┘    └────────────┘  └──┘ 
src                └┘    └────────────┘  └──┘
typ                └┘    └────────────┘  └──┘ 
doc                └┘
 56  { mul_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id                                       └───────────┘
src                                            └───────────┘
typ                                      └───────────┘
 57      (calc ((a * b) % n * c) ≡ a * b * c [MOD n] : modeq_mul (nat.mod_mod _ _) rfl
id                                               └───────┘  └─────────┘      └─┘
src                                               └───────┘  └─────────┘      └─┘
typ                                              └───────┘  └─────────┘      └─┘
 58        ... ≡ a * (b * c) [MOD n] : by rw mul_assoc
id                                         └───────┘
src                                     └─┘└───────┘
typ                                     └─┘└───────┘
doc                                       └─┘         
txt                                       └─┘         
par                                       └─┘         
pid                                                  
st                                       └─────────────
 59        ... ≡ a * (b * c % n) [MOD n] : modeq_mul rfl (nat.mod_mod _ _).symm),
id                                     └───────┘ └─┘  └─────────┘     └──┘
src  ─────┘                             └───────┘ └─┘  └─────────┘     └──┘
typ  ─────┘                            └───────┘ └─┘  └─────────┘     └──┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘
 60    mul_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a * b) % n = (b * a) % n, by rw mul_comm),
id                              └───────────┘                                 └──────┘
src                                 └───────────┘                                └─┘└──────┘
typ                             └───────────┘                              └─┘└──────┘
doc                                                                                   └─┘
txt                                                                                   └─┘
par                                                                                   └─┘
pid                                                                                     
st                                                                                   └──────────┘
 61    ..fin.has_mul }
id       └─────────┘
src      └─────────┘
typ      └─────────┘
 62  
 63  instance (n : ℕ+) : has_one (zmod n) := ⟨⟨(1 % n), nat.mod_lt _ n.pos⟩⟩
id                 └┘    └─────┘  └──┘               └────────┘   └──┘
src                └┘    └─────┘  └──┘                 └────────┘    └──┘
typ                └┘    └─────┘  └──┘               └────────┘   └──┘
doc                └┘
 64  
 65  instance (n : ℕ+) : has_zero (zmod n) := ⟨⟨0, n.pos⟩⟩
id                 └┘    └──────┘  └──┘           └──┘
src                └┘    └──────┘  └──┘             └──┘
typ                └┘    └──────┘  └──┘           └──┘
doc                └┘
 66  
 67  instance (n : ℕ+) : inhabited (zmod n) := ⟨0⟩
id                 └┘    └───────┘  └──┘ 
src                └┘    └───────┘  └──┘
typ                └┘    └───────┘  └──┘ 
doc                └┘
 68  
 69  instance zmod_one.subsingleton : subsingleton (zmod 1) :=
id                                    └──────────┘  └──┘
src                                   └──────────┘  └──┘
typ                                   └──────────┘  └──┘
 70  ⟨λ a b, fin.eq_of_veq (by rw [eq_zero_of_le_zero (le_of_lt_succ a.2),
id         └───────────┘         └────────────────┘  └───────────┘ 
src          └───────────┘     └──┘└────────────────┘ └───────────┘ └────
typ        └───────────┘     └──┘└────────────────┘ └───────────┘└────
doc                            └──┘                                 └────
txt                            └──┘                                 └────
par                            └──┘                                 └────
pid                              └┘                                 └────
st                            └─────────────────────────────────────────┘└─
 71    eq_zero_of_le_zero (le_of_lt_succ b.2)])⟩
id     └────────────────┘  └───────────┘ 
src  ─┘└────────────────┘ └───────────┘ └──┘
typ  ─┘└────────────────┘ └───────────┘└──┘
doc  ─┘                                 └──┘
txt  ─┘                                 └──┘
par  ─┘                                 └──┘
pid  ─┘                                 └──┘
st   ───────────────────────────────────────┘
 72  
 73  lemma add_val {n : ℕ+} : ∀ a b : zmod n, (a + b).val = (a.val + b.val) % n
id                      └┘           └──┘       └─┘    └──┘  └──┘   
src                     └┘            └──┘          └─┘     └──┘   └──┘  
typ                     └┘           └──┘       └─┘    └──┘  └──┘   
doc                     └┘
 74  | ⟨_, _⟩ ⟨_, _⟩ := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
 75  
 76  lemma mul_val {n : ℕ+} :  ∀ a b : zmod n, (a * b).val = (a.val * b.val) % n
id                      └┘            └──┘       └─┘    └──┘  └──┘   
src                     └┘             └──┘          └─┘     └──┘   └──┘  
typ                     └┘            └──┘       └─┘    └──┘  └──┘   
doc                     └┘
 77  | ⟨_, _⟩ ⟨_, _⟩ := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
 78  
 79  lemma one_val {n : ℕ+} : (1 : zmod n).val = 1 % n := rfl
id                      └┘         └──┘  └─┘          └─┘
src                     └┘         └──┘   └─┘           └─┘
typ                     └┘         └──┘  └─┘          └─┘
doc                     └┘
 80  
 81  @[simp] lemma zero_val (n : ℕ+) : (0 : zmod n).val = 0 := rfl
id                               └┘         └──┘  └─┘        └─┘
src                              └┘         └──┘   └─┘        └─┘
typ                              └┘         └──┘  └─┘        └─┘
doc    └──┘                      └┘
 82  
 83  private lemma one_mul_aux (n : ℕ+) (a : zmod n) : (1 : zmod n) * a = a :=
id                                  └┘       └──┘          └──┘      
src                                 └┘       └──┘           └──┘       
typ                                 └┘       └──┘          └──┘      
doc                                 └┘
 84  begin
st   └─────
 85    cases n with n hn,
id           
src    └────┘ └────────┘
typ    └────┘└────────┘
doc    └────┘ └────────┘
txt    └────┘ └────────┘
par    └────┘ └────────┘
pid          └────────┘
st   ──────────────────┘└─
 86    cases n with n,
id           
src    └────┘ └─────┘
typ    └────┘└─────┘
doc    └────┘ └─────┘
txt    └────┘ └─────┘
par    └────┘ └─────┘
pid          └─────┘
st   ───────────────┘└─
 87    { exact (lt_irrefl _ hn).elim },
id              └───────┘   └┘
src      └────┘ └───────┘└─┘  └─────┘
typ      └────┘ └───────┘└─┘└┘└─────┘
doc      └────┘          └─┘  └─────┘
txt      └────┘          └─┘  └─────┘
par      └────┘          └─┘  └─────┘
pid                     └─┘  └───┘└┘
st   ───┘└──────────────────────────┘└┘
 88    { cases n with n,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
 89      { exact @subsingleton.elim (zmod 1) _ _ _ },
id                └───────────────┘  └──┘
src        └────┘ └───────────────┘ └──┘└────────┘
typ        └────┘ └───────────────┘ └──┘└────────┘
doc        └────┘                       └────────┘
txt        └────┘                       └────────┘
par        └────┘                       └────────┘
pid                                    └───────┘
st   ─────┘└──────────────────────────────────────┘└┘
 90      { have h₁ : a.1 % n.succ.succ = a.1 := nat.mod_eq_of_lt a.2,
id                        └─────────┘        └──────────────┘ 
src        └────────┘ └─┘└─────────┘ └────┘└──────────────┘ └┘
typ        └────────┘ └─┘└─────────┘└────┘└──────────────┘└┘
doc        └────────┘ └─┘              └────┘                 └┘
txt        └────────┘ └─┘              └────┘                 └┘
par        └────────┘ └─┘              └────┘                 └┘
pid        └─────┘└─┘ └─┘              └────┘                 └┘
st   ──────────────────────────────────────────────────────────────┘└─
 91        have h₂ : 1 % n.succ.succ = 1 := nat.mod_eq_of_lt dec_trivial,
id                       └─────────┘        └──────────────┘ └─────────┘
src        └──────────┘ └─────────┘ └────┘└──────────────┘└─────────┘
typ        └──────────┘ └─────────┘ └────┘└──────────────┘└─────────┘
doc        └──────────┘             └────┘                └─────────┘
txt        └──────────┘             └────┘                
par        └──────────┘             └────┘                
pid        └─────┘└───┘             └───┘                
st   ──────────────────────────────────────────────────────────────────┘└─
 92        refine fin.eq_of_veq _,
id                └───────────┘
src        └─────┘└───────────┘└┘
typ        └─────┘└───────────┘└┘
doc        └─────┘             └┘
txt        └─────┘             └┘
par        └─────┘             └┘
pid                           └┘
st   ───────────────────────────┘└─
 93        simp [mul_val, one_val, h₁, h₂] } }
id               └─────┘  └─────┘  └┘  └┘
src        └────┘└─────┘└┘└─────┘└┘  └┘  └┘
typ        └────┘└─────┘└┘└─────┘└┘└┘└┘└┘└┘
doc        └────┘       └┘       └┘  └┘  └┘
txt        └────┘       └┘       └┘  └┘  └┘
par        └────┘       └┘       └┘  └┘  └┘
pid                   └┘       └┘  └┘  
st   ─────────────────────────────────────┘└───
 94  end
st   ──┘
 95  
 96  private lemma left_distrib_aux (n : ℕ+) : ∀ a b c : zmod n, a * (b + c) = a * b + a * c :=
id                                       └┘              └──┘                 
src                                      └┘              └──┘                       
typ                                      └┘              └──┘                 
doc                                      └┘
 97  λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id                        └───────────┘
src                             └───────────┘
typ                       └───────────┘
 98  (calc a * ((b + c) % n) ≡ a * (b + c) [MOD n] : modeq_mul rfl (nat.mod_mod _ _)
id                                             └───────┘ └─┘  └─────────┘
src                                             └───────┘ └─┘  └─────────┘
typ                                            └───────┘ └─┘  └─────────┘
 99    ... ≡ a * b + a * c [MOD n] : by rw mul_add
id                                      └─────┘
src                                  └─┘└─────┘
typ                                  └─┘└─────┘
doc                                     └─┘       
txt                                     └─┘       
par                                     └─┘       
pid                                              
st                                     └───────────
100    ... ≡ (a * b) % n + (a * c) % n [MOD n] : modeq_add (nat.mod_mod _ _).symm (nat.mod_mod _ _).symm)
id                                        └───────┘  └─────────┘     └──┘   └─────────┘     └──┘
src  ─┘                                     └───────┘  └─────────┘     └──┘   └─────────┘     └──┘
typ  ─┘                                   └───────┘  └─────────┘     └──┘   └─────────┘     └──┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
101  
102  instance (n : ℕ+) : comm_ring (zmod n) :=
id                 └┘    └───────┘  └──┘ 
src                └┘    └───────┘  └──┘
typ                └┘    └───────┘  └──┘ 
doc                └┘
103  { zero_add := λ ⟨a, ha⟩, fin.eq_of_veq (show (0 + a) % n = a, by rw zero_add; exact nat.mod_eq_of_lt ha),
id                          └───────────┘                          └──────┘        └──────────────┘ └┘
src                           └───────────┘                        └─┘└──────┘  └────┘└──────────────┘
typ                         └───────────┘                       └─┘└──────┘  └────┘└──────────────┘└┘
doc                                                                   └─┘          └────┘                
txt                                                                   └─┘          └────┘                
par                                                                   └─┘          └────┘                
pid                                                                                                    
st                                                                   └─────────────────────────────────────┘
104    add_zero := λ ⟨a, ha⟩, fin.eq_of_veq (nat.mod_eq_of_lt ha),
id                      └┘   └───────────┘  └──────────────┘
src                           └───────────┘  └──────────────┘
typ                     └┘   └───────────┘  └──────────────┘
105    add_left_neg :=
106      λ ⟨a, ha⟩, fin.eq_of_veq (show (((-a : ℤ) % n).to_nat + a) % n = 0,
id                └───────────┘                  └────┘        
src                 └───────────┘                   └────┘         
typ               └───────────┘                  └────┘        
107        from int.coe_nat_inj
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
108        begin
st         └─────
109          have hn : (n : ℤ) ≠ 0 := (ne_of_lt (int.coe_nat_lt.2 n.pos)).symm,
id                                  └──────┘  └────────────┘   └───┘
src          └────────┘  └─┘└┘└────┘ └──────┘ └────────────┘└─┘└───┘└─────┘
typ          └────────┘ └─┘└┘└────┘ └──────┘ └────────────┘└─┘└───┘└─────┘
doc          └────────┘  └─┘ └┘ └────┘                        └─┘     └─────┘
txt          └────────┘  └─┘ └┘ └────┘                        └─┘     └─────┘
par          └────────┘  └─┘ └┘ └────┘                        └─┘     └─────┘
pid          └─────┘└─┘  └─┘ └┘ └───┘                        └─┘     └────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
110          rw [int.coe_nat_mod, int.coe_nat_add, to_nat_of_nonneg (int.mod_nonneg _ hn), add_comm],
id               └─────────────┘  └─────────────┘  └──────────────┘  └────────────┘   └┘   └──────┘
src          └──┘└─────────────┘└┘└─────────────┘└┘└──────────────┘ └────────────┘└─┘  └─┘└──────┘
typ          └──┘└─────────────┘└┘└─────────────┘└┘└──────────────┘ └────────────┘└─┘└┘└─┘└──────┘
doc          └──┘               └┘               └┘                               └─┘  └─┘        
txt          └──┘               └┘               └┘                               └─┘  └─┘        
par          └──┘               └┘               └┘                               └─┘  └─┘        
pid            └┘               └┘               └┘                               └─┘  └─┘        
st   ──────────────────────────┘└───────────────┘└──────────────────────────────────────┘└────────┘└──
111          simp,
src          └──┘
typ          └──┘
doc          └──┘
txt          └──┘
par          └──┘
st   ───────────┘└─
112        end),
st   ────────┘
113    one_mul := one_mul_aux n,
id                └─────────┘ 
src               └─────────┘
typ               └─────────┘ 
114    mul_one := λ a, by rw mul_comm; exact one_mul_aux n a,
id                          └──────┘        └─────────┘  
src                       └─┘└──────┘  └────┘└─────────┘ 
typ                      └─┘└──────┘  └────┘└─────────┘
doc                       └─┘          └────┘            
txt                       └─┘          └────┘            
par                       └─┘          └────┘            
pid                                                    
st                       └─────────────────────────────────┘
115    left_distrib := left_distrib_aux n,
id                     └──────────────┘ 
src                    └──────────────┘
typ                    └──────────────┘ 
116    right_distrib := λ a b c, by rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]; refl,
id                                   └──────┘  └──────────────┘  └──────┘     └──────┘
src                                 └──┘└──────┘└┘└──────────────┘└┘└──────┘└─┘ └┘└──────┘  └──┘
typ                              └──┘└──────┘└┘└──────────────┘└┘└──────┘└─┘└┘└──────┘  └──┘
doc                                 └──┘        └┘                └┘        └─┘ └┘          └──┘
txt                                 └──┘        └┘                └┘        └─┘ └┘          └──┘
par                                 └──┘        └┘                └┘        └─┘ └┘          └──┘
pid                                   └┘        └┘                └┘        └─┘ └┘        
st                                 └───────────┘└────────────────┘└────────────┘└────────┘└────┘
117    ..zmod.has_zero n,
id       └───────────┘ 
src      └───────────┘
typ      └───────────┘ 
118    ..zmod.has_one n,
id       └──────────┘ 
src      └──────────┘
typ      └──────────┘ 
119    ..zmod.has_neg n,
id       └──────────┘ 
src      └──────────┘
typ      └──────────┘ 
120    ..zmod.add_comm_semigroup n,
id       └─────────────────────┘ 
src      └─────────────────────┘
typ      └─────────────────────┘ 
121    ..zmod.comm_semigroup n }
id       └─────────────────┘ 
src      └─────────────────┘
typ      └─────────────────┘ 
122  
123  lemma val_cast_nat {n : ℕ+} (a : ℕ) : (a : zmod n).val = a % n :=
id                           └┘               └──┘  └─┘     
src                          └┘                └──┘   └─┘     
typ                          └┘               └──┘  └─┘     
doc                          └┘
124  begin
st   └─────
125    induction a with a ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
126    { rw [nat.zero_mod]; refl },
id           └──────────┘
src      └──┘└──────────┘  └───┘
typ      └──┘└──────────┘  └───┘
doc      └──┘              └───┘
txt      └──┘              └───┘
par      └──┘              └───┘
pid        └┘                  
st   ───┘└──────────────┘└─────┘└┘
127    { rw [succ_eq_add_one, nat.cast_add, add_val, ih],
id           └─────────────┘  └──────────┘  └─────┘  └┘
src      └──┘└─────────────┘└┘└──────────┘└┘└─────┘└┘  
typ      └──┘└─────────────┘└┘└──────────┘└┘└─────┘└┘└┘
doc      └──┘               └┘            └┘       └┘  
txt      └──┘               └┘            └┘       └┘  
par      └──┘               └┘            └┘       └┘  
pid        └┘               └┘            └┘       └┘  
st   ──────────────────────┘└────────────┘└───────┘└──┘└─
128      show (a % n + ((0 + (1 % n)) % n)) % n = (a + 1) % n,
id                                                      
src      └───┘     └┘  └┘  └─┘  └─┘     └──┘ 
typ      └───┘     └┘  └┘  └─┘  └─┘    └──┘ 
doc      └───┘       └┘  └┘  └─┘  └─┘      └──┘ 
txt      └───┘       └┘  └┘  └─┘  └─┘      └──┘ 
par      └───┘       └┘  └┘  └─┘  └─┘      └──┘ 
pid      └───┘       └┘  └┘  └─┘  └─┘      └──┘ 
st   ───────────────────────────────────────────────────────┘└─
129      rw [zero_add, nat.mod_mod],
id           └──────┘  └─────────┘
src      └──┘└──────┘└┘└─────────┘
typ      └──┘└──────┘└┘└─────────┘
doc      └──┘        └┘           
txt      └──┘        └┘           
par      └──┘        └┘           
pid        └┘        └┘           
st   ───────────────┘└───────────┘└──
130      exact nat.modeq.modeq_add (nat.mod_mod a n) (nat.mod_mod 1 n) }
id             └─────────────────┘                   └─────────┘   
src      └────┘└─────────────────┘              └┘ └─────────┘└─┘ └┘
typ      └────┘└─────────────────┘             └┘ └─────────┘└─┘└┘
doc      └────┘                                 └┘            └─┘ └┘
txt      └────┘                                 └┘            └─┘ └┘
par      └────┘                                 └┘            └─┘ └┘
pid                                            └┘            └─┘ 
st   ─────────────────────────────────────────────────────────────────┘└─
131  end
st   ──┘
132  
133  lemma neg_val' {m : pnat} (n : zmod m) : (-n).val = (m - n.val) % m :=
id                       └──┘       └──┘       └─┘      └──┘   
src                      └──┘       └──┘         └─┘        └──┘  
typ                      └──┘       └──┘       └─┘      └──┘   
doc                      └──┘
134  have ((-n).val + n.val) % m = (m - n.val + n.val) % m,
id           └─┘   └──┘        └──┘  └──┘   
src           └─┘    └──┘           └──┘   └──┘  
typ          └─┘   └──┘        └──┘  └──┘   
135    by { rw [←add_val, add_left_neg, nat.sub_add_cancel (le_of_lt n.is_lt), nat.mod_self], refl },
id               └─────┘  └──────────┘  └────────────────┘  └──────┘ └─────┘   └──────────┘
src         └───┘└─────┘└┘└──────────┘└┘└────────────────┘ └──────┘└─────┘└─┘└──────────┘  └───┘
typ         └───┘└─────┘└┘└──────────┘└┘└────────────────┘ └──────┘└─────┘└─┘└──────────┘  └───┘
doc         └───┘       └┘            └┘                                  └─┘              └───┘
txt         └───┘       └┘            └┘                                  └─┘              └───┘
par         └───┘       └┘            └┘                                  └─┘              └───┘
pid           └─┘       └┘            └┘                                  └─┘                  
st       └─────────────┘└────────────┘└─────────────────────────────────────┘└────────────┘└──────┘└┘
136  (nat.mod_eq_of_lt (fin.is_lt _)).symm.trans (nat.modeq.modeq_add_cancel_right rfl this)
id    └──────────────┘  └───────┘    └──┘ └───┘   └──────────────────────────────┘ └─┘ └──┘
src   └──────────────┘  └───────┘    └──┘ └───┘   └──────────────────────────────┘ └─┘
typ   └──────────────┘  └───────┘    └──┘ └───┘   └──────────────────────────────┘ └─┘ └──┘
137  
138  lemma neg_val {m : pnat} (n : zmod m) : (-n).val = if n = 0 then 0 else m - n.val :=
id                      └──┘       └──┘       └─┘                        └──┘
src                     └──┘       └──┘         └─┘                           └──┘
typ                     └──┘       └──┘       └─┘                        └──┘
doc                     └──┘
139  begin
st   └─────
140    rw neg_val',
id        └──────┘
src    └─┘└──────┘
typ    └─┘└──────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────┘└─
141    by_cases h : n = 0; simp [h],
id                             
src    └───────┘ └─┘ └┘  └────┘ 
typ    └───────┘ └─┘└┘  └────┘
doc    └───────┘ └─┘  └┘  └────┘ 
txt    └───────┘ └─┘  └┘  └────┘ 
par    └───────┘ └─┘  └┘  └────┘ 
pid             └─┘         
st   ─────────────────────────────┘└─
142    cases n with n nlt; cases n; dsimp, { contradiction },
id                              
src    └────┘ └─────────┘  └────┘   └───┘    └────────────┘
typ    └────┘└─────────┘  └────┘  └───┘    └────────────┘
doc    └────┘ └─────────┘  └────┘   └───┘    └────────────┘
txt    └────┘ └─────────┘  └────┘   └───┘    └────────────┘
par    └────┘ └─────────┘  └────┘   └───┘    └────────────┘
pid          └─────────┘                                
st   ───────────────────────────────────┘└──┘└────────────┘└┘
143    rw nat.mod_eq_of_lt,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
144    apply nat.sub_lt m.2 (nat.succ_pos _),
id           └────────┘     └──────────┘
src    └────┘└────────┘ └─┘ └──────────┘└─┘
typ    └────┘└────────┘└─┘ └──────────┘└─┘
doc    └────┘           └─┘             └─┘
txt    └────┘           └─┘             └─┘
par    └────┘           └─┘             └─┘
pid                    └─┘             └─┘
st   ──────────────────────────────────────┘└─
145  end
st   ──┘
146  
147  lemma mk_eq_cast {n : ℕ+} {a : ℕ} (h : a < n) : (⟨a, h⟩ : zmod n) = (a : zmod n) :=
id                         └┘                            └──┘        └──┘ 
src                        └┘                                └──┘          └──┘
typ                        └┘                            └──┘        └──┘ 
doc                        └┘
148  fin.eq_of_veq (by rw [val_cast_nat, nat.mod_eq_of_lt h])
id   └───────────┘         └──────────┘  └──────────────┘ 
src  └───────────┘     └──┘└──────────┘└┘└──────────────┘ 
typ  └───────────┘     └──┘└──────────┘└┘└──────────────┘
doc                    └──┘            └┘                 
txt                    └──┘            └┘                 
par                    └──┘            └┘                 
pid                      └┘            └┘                 
st                    └───────────────┘└──────────────────┘
149  
150  @[simp] lemma cast_self_eq_zero {n : ℕ+} : ((n : ℕ) : zmod n) = 0 :=
id                                        └┘             └──┘   
src                                       └┘              └──┘    
typ                                       └┘             └──┘   
doc    └──┘                               └┘
151  fin.eq_of_veq (show (n : zmod n).val = 0, by simp [val_cast_nat])
id   └───────────┘           └──┘  └─┘               └──────────┘
src  └───────────┘            └──┘   └─┘         └────┘└──────────┘
typ  └───────────┘           └──┘  └─┘         └────┘└──────────┘
doc                                               └────┘            
txt                                               └────┘            
par                                               └────┘            
pid                                                               
st                                               └──────────────────┘
152  
153  lemma val_cast_of_lt {n : ℕ+} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=
id                             └┘                        └──┘  └─┘   
src                            └┘                           └──┘   └─┘  
typ                            └┘                        └──┘  └─┘   
doc                            └┘
154  by rw [val_cast_nat, nat.mod_eq_of_lt h]
id          └──────────┘  └──────────────┘ 
src     └──┘└──────────┘└┘└──────────────┘ └─
typ     └──┘└──────────┘└┘└──────────────┘└─
doc     └──┘            └┘                 └─
txt     └──┘            └┘                 └─
par     └──┘            └┘                 └─
pid       └┘            └┘                 
st     └───────────────┘└──────────────────┘
155  
src  
typ  
doc  
txt  
par  
pid  
st   
156  @[simp] lemma cast_mod_nat (n : ℕ+) (a : ℕ) : ((a % n : ℕ) : zmod n) = a :=
id                                   └┘                      └──┘    
src                                  └┘                        └──┘    
typ                                  └┘                      └──┘    
doc    └──┘                          └┘
157  by conv {to_rhs, rw ← nat.mod_add_div a n}; simp
id                         └─────────────┘  
src     └────┘└────┘└┘└───┘└─────────────┘    └────
typ     └────┘└────┘└┘└───┘└─────────────┘  └────
doc                                              └────
txt     └────┘└────┘└┘└───┘                   └────
par     └────┘└────┘└┘└───┘                   └────
pid         └────────────┘                       
st     └─────┘└────┘└────────────────────────┘└┘└─────
158  
src  
typ  
doc  
txt  
par  
pid  
st   
159  @[simp] lemma cast_mod_nat' {n : ℕ} (hn : 0 < n) (a : ℕ) : ((a % n : ℕ) : zmod ⟨n, hn⟩) = a :=
id                                                                     └──┘    └┘    
src                                                                       └──┘          
typ                                                                    └──┘    └┘    
doc    └──┘
160  cast_mod_nat _ _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
161  
162  @[simp] lemma cast_val {n : ℕ+} (a : zmod n) : (a.val : zmod n) = a :=
id                               └┘       └──┘      └──┘   └──┘    
src                              └┘       └──┘        └──┘   └──┘    
typ                              └┘       └──┘      └──┘   └──┘    
doc    └──┘                      └┘
163  by cases a; simp [mk_eq_cast]
id                    └────────┘
src     └────┘   └────┘└────────┘└─
typ     └────┘  └────┘└────────┘└─
doc     └────┘   └────┘          └─
txt     └────┘   └────┘          └─
par     └────┘   └────┘          └─
pid                           
st     └───────────────────────────
164  
src  
typ  
doc  
txt  
par  
pid  
st   
165  @[simp] lemma cast_mod_int (n : ℕ+) (a : ℤ) : ((a % (n : ℕ) : ℤ) : zmod n) = a :=
id                                   └┘                           └──┘    
src                                  └┘                             └──┘    
typ                                  └┘                           └──┘    
doc    └──┘                          └┘
166  by conv {to_rhs, rw ← int.mod_add_div a n}; simp
id                         └─────────────┘  
src     └────┘└────┘└┘└───┘└─────────────┘    └────
typ     └────┘└────┘└┘└───┘└─────────────┘  └────
doc                                              └────
txt     └────┘└────┘└┘└───┘                   └────
par     └────┘└────┘└┘└───┘                   └────
pid         └────────────┘                       
st     └─────┘└────┘└────────────────────────┘└┘└─────
167  
src  
typ  
doc  
txt  
par  
pid  
st   
168  @[simp] lemma cast_mod_int' {n : ℕ} (hn : 0 < n) (a : ℤ) :
id                                                      
src                                                      
typ                                                     
doc    └──┘
169    ((a % (n : ℕ) : ℤ) : zmod ⟨n, hn⟩) = a := cast_mod_int _ _
id                     └──┘    └┘        └──────────┘
src                      └──┘                └──────────┘
typ                    └──┘    └┘        └──────────┘
170  
171  lemma val_cast_int {n : ℕ+} (a : ℤ) : (a : zmod n).val = (a % (n : ℕ)).nat_abs :=
id                           └┘               └──┘  └─┘            └─────┘
src                          └┘                └──┘   └─┘              └─────┘
typ                          └┘               └──┘  └─┘            └─────┘
doc                          └┘
172  have h : nat_abs (a % (n : ℕ)) < n := int.coe_nat_lt.1 begin
id            └─────┘                └────────────┘
src           └─────┘                   └────────────┘
typ           └─────┘                └────────────┘
st                                                          └─────
173    rw [nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))],
id         └───────────────┘  └────────┘    └─────────────────────────┘   └───┘
src    └──┘└───────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└─┘
typ    └──┘└───────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└─┘
doc    └──┘                            └─┘                            └─┘     └─┘
txt    └──┘                            └─┘                            └─┘     └─┘
par    └──┘                            └─┘                            └─┘     └─┘
pid      └┘                            └─┘                            └─┘     └─┘
st   ───────────────────────────────────────────────────────────────────────────┘└──
174    conv {to_rhs, rw ← abs_of_nonneg (int.coe_nat_nonneg n)},
id                        └───────────┘  └────────────────┘ 
src    └────┘└────┘└┘└───┘└───────────┘ └────────────────┘ 
typ    └────┘└────┘└┘└───┘└───────────┘ └────────────────┘
txt    └────┘└────┘└┘└───┘                                 
par    └────┘└────┘└┘└───┘                                 
pid        └────────────┘                                 └┘
st   ───────┘└────┘└─────────────────────────────────────────┘└┘
175    exact int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)
id           └────────┘    └─────────────────────────┘   └───┘
src    └────┘└────────┘└─┘ └─────────────────────────┘└─┘└───┘└┘
typ    └────┘└────────┘└─┘ └─────────────────────────┘└─┘└───┘└┘
doc    └────┘          └─┘                            └─┘     └┘
txt    └────┘          └─┘                            └─┘     └┘
par    └────┘          └─┘                            └─┘     └┘
pid                   └─┘                            └─┘     
st   ──────────────────────────────────────────────────────────┘
176  end,
st   └─┘
177  int.coe_nat_inj $
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
178    by conv {to_lhs, rw [← cast_mod_int n a,
id                            └──────────┘  
src       └────┘└────┘└┘└────┘└──────────┘  └─
typ       └────┘└────┘└┘└────┘└──────────┘└─
txt       └────┘└────┘└┘└────┘              └─
par       └────┘└────┘└┘└────┘              └─
pid           └─────────────┘              └─
st       └─────┘└────┘└──────────────────────┘└─
179      ← nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
id         └───────────────┘  └────────┘    └─────────────────────────┘   └───┘
src  ─────┘└───────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ  ─────┘└───────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
txt  ─────┘                            └─┘                            └─┘     └───
par  ─────┘                            └─┘                            └─┘     └───
pid  ─────┘                            └─┘                            └─┘     └───
st   ───────────────────────────────────────────────────────────────────────────┘└─
180      int.cast_coe_nat, val_cast_of_lt h] }
id       └──────────────┘  └────────────┘ 
src  ───┘└──────────────┘└┘└────────────┘ └┘└─
typ  ───┘└──────────────┘└┘└────────────┘└┘└─
txt  ───┘                └┘               └┘└─
par  ───┘                └┘               └┘└─
pid  ───┘                └┘               └─┘
st   ───────────────────┘└────────────────┘ 
181  
src  
typ  
txt  
par  
pid  
st   
182  lemma coe_val_cast_int {n : ℕ+} (a : ℤ) : ((a : zmod n).val : ℤ) = a % (n : ℕ) :=
id                               └┘                └──┘  └─┘             
src                              └┘                 └──┘   └─┘               
typ                              └┘                └──┘  └─┘             
doc                              └┘
183  by rw [val_cast_int, int.nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))]
id          └──────────┘  └───────────────────┘  └────────┘    └─────────────────────────┘   └───┘
src     └──┘└──────────┘└┘└───────────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ     └──┘└──────────┘└┘└───────────────────┘ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
doc     └──┘            └┘                                └─┘                            └─┘     └───
txt     └──┘            └┘                                └─┘                            └─┘     └───
par     └──┘            └┘                                └─┘                            └─┘     └───
pid       └┘            └┘                                └─┘                            └─┘     └─┘
st     └───────────────┘└──────────────────────────────────────────────────────────────────────────┘
184  
src  
typ  
doc  
txt  
par  
pid  
st   
185  lemma eq_iff_modeq_nat {n : ℕ+} {a b : ℕ} : (a : zmod n) = b ↔ a ≡ b [MOD n] :=
id                               └┘                 └──┘         └──┘ 
src                              └┘                  └──┘             └──┘  
typ                              └┘                 └──┘         └──┘ 
doc                              └┘                                      └──┘  
186  ⟨λ h, by have := fin.veq_of_eq h;
id                   └───────────┘ 
src           └──────┘└───────────┘
typ          └──────┘└───────────┘
doc           └──────┘             
txt           └──────┘             
par           └──────┘             
pid           └───┘└─┘             
st           └─────────────────────────
187    rwa [val_cast_nat, val_cast_nat] at this,
id          └──────────┘  └──────────┘
src    └───┘└──────────┘└┘└──────────┘└───────┘
typ    └───┘└──────────┘└┘└──────────┘└───────┘
doc    └───┘            └┘            └───────┘
txt    └───┘            └┘            └───────┘
par    └───┘            └┘            └───────┘
pid       └┘            └┘            └──────┘
st   ──────┘└──────────┘└────────────┘└──────┘
188  λ h, fin.eq_of_veq $ by rwa [val_cast_nat, val_cast_nat]⟩
id       └───────────┘           └──────────┘  └──────────┘
src       └───────────┘      └───┘└──────────┘└┘└──────────┘
typ      └───────────┘      └───┘└──────────┘└┘└──────────┘
doc                          └───┘            └┘            
txt                          └───┘            └┘            
par                          └───┘            └┘            
pid                             └┘            └┘            
st                          └────────────────┘└────────────┘
189  
190  lemma eq_iff_modeq_nat' {n : ℕ} (hn : 0 < n) {a b : ℕ} : (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [MOD n] :=
id                                                            └──┘    └┘         └──┘ 
src                                                             └──┘                   └──┘  
typ                                                           └──┘    └┘         └──┘ 
doc                                                                                         └──┘  
191  eq_iff_modeq_nat
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
192  
193  lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] :=
id                               └┘                 └──┘         └───┘      
src                              └┘                  └──┘             └───┘       
typ                              └┘                 └──┘         └───┘      
doc                              └┘
194  ⟨λ h, by have := fin.veq_of_eq h;
id                   └───────────┘ 
src           └──────┘└───────────┘
typ          └──────┘└───────────┘
doc           └──────┘             
txt           └──────┘             
par           └──────┘             
pid           └───┘└─┘             
st           └─────────────────────────
195    rwa [val_cast_int, val_cast_int, ← int.coe_nat_eq_coe_nat_iff,
id          └──────────┘  └──────────┘    └────────────────────────┘
src    └───┘└──────────┘└┘└──────────┘└──┘└────────────────────────┘└─
typ    └───┘└──────────┘└┘└──────────┘└──┘└────────────────────────┘└─
doc    └───┘            └┘            └──┘                          └─
txt    └───┘            └┘            └──┘                          └─
par    └───┘            └┘            └──┘                          └─
pid       └┘            └┘            └──┘                          └─
st   ──────┘└──────────┘└────────────┘└────────────────────────────┘└─
196      nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
id       └───────────────┘  └────────────┘    └─────────────────────────┘   └───┘
src  ───┘└───────────────┘ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ  ───┘└───────────────┘ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
doc  ───┘                                └─┘                            └─┘     └───
txt  ───┘                                └─┘                            └─┘     └───
par  ───┘                                └─┘                            └─┘     └───
pid  ───┘                                └─┘                            └─┘     └───
st   ─────────────────────────────────────────────────────────────────────────────┘└─
197      nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))] at this,
id       └───────────────┘  └────────────┘    └─────────────────────────┘   └───┘
src  ───┘└───────────────┘ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└─────────┘
typ  ───┘└───────────────┘ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└─────────┘
doc  ───┘                                └─┘                            └─┘     └─────────┘
txt  ───┘                                └─┘                            └─┘     └─────────┘
par  ───┘                                └─┘                            └─┘     └─────────┘
pid  ───┘                                └─┘                            └─┘     └─┘└──────┘
st   ─────────────────────────────────────────────────────────────────────────────┘└──────┘
198  λ h : a % (n : ℕ) = b % (n : ℕ),
id                        
src                           
typ                       
199    by rw [← cast_mod_int n a, ← cast_mod_int n b, h]⟩
id              └──────────┘      └──────────┘    
src       └────┘└──────────┘  └──┘└──────────┘  └┘ 
typ       └────┘└──────────┘└──┘└──────────┘└┘
doc       └────┘              └──┘              └┘ 
txt       └────┘              └──┘              └┘ 
par       └────┘              └──┘              └┘ 
pid         └──┘              └──┘              └┘ 
st       └─────────────────────┘└──────────────────┘└─┘
200  
201  lemma eq_iff_modeq_int' {n : ℕ} (hn : 0 < n) {a b : ℤ} :
id                                                    
src                                                    
typ                                                   
202    (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [ZMOD (n : ℕ)] := eq_iff_modeq_int
id         └──┘    └┘         └───┘          └──────────────┘
src         └──┘                   └───┘           └──────────────┘
typ        └──┘    └┘         └───┘          └──────────────┘
203  
204  lemma eq_zero_iff_dvd_nat {n : ℕ+} {a : ℕ} : (a : zmod n) = 0 ↔ (n : ℕ) ∣ a :=
id                                  └┘               └──┘              
src                                 └┘                └──┘               
typ                                 └┘               └──┘              
doc                                 └┘
205  by rw [← @nat.cast_zero (zmod n), eq_iff_modeq_nat, nat.modeq.modeq_zero_iff]
id             └───────────┘  └──┘    └──────────────┘  └──────────────────────┘
src     └────┘ └───────────┘ └──┘ └─┘└──────────────┘└┘└──────────────────────┘└─
typ     └────┘ └───────────┘ └──┘└─┘└──────────────┘└┘└──────────────────────┘└─
doc     └────┘                    └─┘                └┘                        └─
txt     └────┘                    └─┘                └┘                        └─
par     └────┘                    └─┘                └┘                        └─
pid       └──┘                    └─┘                └┘                        
st     └────────────────────────────┘└────────────────┘└────────────────────────┘
206  
src  
typ  
doc  
txt  
par  
pid  
st   
207  lemma eq_zero_iff_dvd_int {n : ℕ+} {a : ℤ} : (a : zmod n) = 0 ↔ ((n : ℕ) : ℤ) ∣ a :=
id                                  └┘               └──┘                   
src                                 └┘                └──┘                    
typ                                 └┘               └──┘                   
doc                                 └┘
208  by rw [← @int.cast_zero (zmod n), eq_iff_modeq_int, int.modeq.modeq_zero_iff]
id             └───────────┘  └──┘    └──────────────┘  └──────────────────────┘
src     └────┘ └───────────┘ └──┘ └─┘└──────────────┘└┘└──────────────────────┘└─
typ     └────┘ └───────────┘ └──┘└─┘└──────────────┘└┘└──────────────────────┘└─
doc     └────┘                    └─┘                └┘                        └─
txt     └────┘                    └─┘                └┘                        └─
par     └────┘                    └─┘                └┘                        └─
pid       └──┘                    └─┘                └┘                        
st     └────────────────────────────┘└────────────────┘└────────────────────────┘
209  
src  
typ  
doc  
txt  
par  
pid  
st   
210  instance (n : ℕ+) : fintype (zmod n) := fin.fintype _
id                 └┘    └─────┘  └──┘      └─────────┘
src                └┘    └─────┘  └──┘       └─────────┘
typ                └┘    └─────┘  └──┘      └─────────┘
doc                └┘    └─────┘
211  
212  instance decidable_eq (n : ℕ+) : decidable_eq (zmod n) := fin.decidable_eq _
id                              └┘    └──────────┘  └──┘      └──────────────┘
src                             └┘    └──────────┘  └──┘       └──────────────┘
typ                             └┘    └──────────┘  └──┘      └──────────────┘
doc                             └┘
213  
214  instance (n : ℕ+) : has_repr (zmod n) := fin.has_repr _
id                 └┘    └──────┘  └──┘      └──────────┘
src                └┘    └──────┘  └──┘       └──────────┘
typ                └┘    └──────┘  └──┘      └──────────┘
doc                └┘
215  
216  lemma card_zmod (n : ℕ+) : fintype.card (zmod n) = n := fintype.card_fin n
id                        └┘    └──────────┘  └──┘        └──────────────┘ 
src                       └┘    └──────────┘  └──┘          └──────────────┘
typ                       └┘    └──────────┘  └──┘        └──────────────┘ 
doc                       └┘    └──────────┘
217  
218  lemma le_div_two_iff_lt_neg {n : ℕ+} (hn : (n : ℕ) % 2 = 1)
id                                    └┘                 
src                                   └┘                  
typ                                   └┘                 
doc                                   └┘
219    {x : zmod n} (hx0 : x ≠ 0) : x.1 ≤ (n / 2 : ℕ) ↔ (n / 2 : ℕ) < (-x).1 :=
id          └──┘                                          
src         └──┘                                                
typ         └──┘                                          
220  have hn2 : (n : ℕ) / 2 < n := nat.div_lt_of_lt_mul ((lt_mul_iff_one_lt_left n.pos).2 dec_trivial),
id                            └──────────────────┘   └────────────────────┘ └──┘   └─────────┘
src                             └──────────────────┘   └────────────────────┘  └──┘   └─────────┘
typ                           └──────────────────┘   └────────────────────┘ └──┘   └─────────┘
doc                                                                                       └─────────┘
221  have hn2' : (n : ℕ) - n / 2 = n / 2 + 1,
id                               
src                                 
typ                              
222    by conv {to_lhs, congr, rw [← succ_sub_one n, succ_sub n.pos]};
id                                   └──────────┘   └──────┘ └───┘
src       └────┘└────┘└┘└───┘└┘└────┘└──────────┘ └┘└──────┘└───┘
typ       └────┘└────┘└┘└───┘└┘└────┘└──────────┘└┘└──────┘└───┘
txt       └────┘└────┘└┘└───┘└┘└────┘             └┘             
par       └────┘└────┘└┘└───┘└┘└────┘             └┘             
pid           └────────────────────┘             └┘             └┘
st       └─────┘└────┘└─────┘└────────────────────┘└──────────────┘ └┘
223    rw [← two_mul_odd_div_two hn, two_mul, ← succ_add, nat.add_sub_cancel],
id           └─────────────────┘ └┘  └─────┘    └──────┘  └────────────────┘
src    └────┘└─────────────────┘  └┘└─────┘└──┘└──────┘└┘└────────────────┘
typ    └────┘└─────────────────┘└┘└┘└─────┘└──┘└──────┘└┘└────────────────┘
doc    └────┘                     └┘       └──┘        └┘                  
txt    └────┘                     └┘       └──┘        └┘                  
par    └────┘                     └┘       └──┘        └┘                  
pid      └──┘                     └┘       └──┘        └┘                  
st   ─────┘└──────────────────────┘└───────┘└──────────┘└──────────────────┘
224  have hxn : (n : ℕ) - x.val < n,
id                     └──┘  
src                      └──┘ 
typ                    └──┘  
225    begin
st     └─────
226      rw [nat.sub_lt_iff (le_of_lt x.2) (le_refl _), nat.sub_self],
id           └────────────┘  └──────┘      └─────┘     └──────────┘
src      └──┘└────────────┘ └──────┘ └──┘ └─────┘└───┘└──────────┘
typ      └──┘└────────────┘ └──────┘└──┘ └─────┘└───┘└──────────┘
doc      └──┘                        └──┘        └───┘            
txt      └──┘                        └──┘        └───┘            
par      └──┘                        └──┘        └───┘            
pid        └┘                        └──┘        └───┘            
st   ────────────────────────────────────────────────┘└────────────┘└──
227      rw ← zmod.cast_val x at hx0,
id            └───────────┘ 
src      └───┘└───────────┘ └─────┘
typ      └───┘└───────────┘└─────┘
doc      └───┘              └─────┘
txt      └───┘              └─────┘
par      └───┘              └─────┘
pid        └─┘              └─────┘
st   ──────────────────────────────┘└─
228      exact nat.pos_of_ne_zero (λ h, by simpa [h] using hx0)
id             └────────────────┘                         └─┘
src      └────┘└────────────────┘  └──┘  └─────┘ └──────┘   └─
typ      └────┘└────────────────┘  └──┘  └─────┘└──────┘└─┘└─
doc      └────┘                    └──┘  └─────┘ └──────┘   └─
txt      └────┘                    └──┘  └─────┘ └──────┘   └─
par      └────┘                    └──┘  └─────┘ └──────┘   └─
pid                               └──┘  └──────┘ └──────┘   
st   ────────────────────────────────────┘└──────────────────┘└─
229    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
230  by conv {to_rhs, rw [← nat.succ_le_iff, succ_eq_add_one, ← hn2', ← zero_add (- x), ← zmod.cast_self_eq_zero,
id                          └─────────────┘  └─────────────┘    └──┘    └──────┘        └────────────────────┘
src     └────┘└────┘└┘└────┘└─────────────┘└┘└─────────────┘└──┘    └──┘└──────┘  └───┘└────────────────────┘└─
typ     └────┘└────┘└┘└────┘└─────────────┘└┘└─────────────┘└──┘└──┘└──┘└──────┘ └───┘└────────────────────┘└─
txt     └────┘└────┘└┘└────┘               └┘               └──┘    └──┘           └───┘                      └─
par     └────┘└────┘└┘└────┘               └┘               └──┘    └──┘           └───┘                      └─
pid         └─────────────┘               └┘               └──┘    └──┘           └───┘                      └─
st     └─────┘└────┘└─────────────────────┘└───────────────┘└──────┘└────────────────┘└────────────────────────┘└─
231    ← sub_eq_add_neg, ← zmod.cast_val x, ← nat.cast_sub (le_of_lt x.2),
id       └────────────┘    └───────────┘     └──────────┘  └──────┘ 
src  ───┘└────────────┘└──┘└───────────┘ └──┘└──────────┘ └──────┘ └────
typ  ───┘└────────────┘└──┘└───────────┘└──┘└──────────┘ └──────┘└────
txt  ───┘              └──┘              └──┘                      └────
par  ───┘              └──┘              └──┘                      └────
pid  ───┘              └──┘              └──┘                      └────
st   ─────────────────┘└─────────────────┘└─────────────────────────────┘└─
232    zmod.val_cast_nat, mod_eq_of_lt hxn, nat.sub_le_sub_left_iff (le_of_lt x.2)] }
id     └───────────────┘  └──────────┘ └─┘  └─────────────────────┘  └──────┘ 
src  ─┘└───────────────┘└┘└──────────┘   └┘└─────────────────────┘ └──────┘ └───┘└─
typ  ─┘└───────────────┘└┘└──────────┘└─┘└┘└─────────────────────┘ └──────┘└───┘└─
txt  ─┘                 └┘               └┘                                 └───┘└─
par  ─┘                 └┘               └┘                                 └───┘└─
pid  ─┘                 └┘               └┘                                 └────┘
st   ──────────────────┘└────────────────┘└──────────────────────────────────────┘ 
233  
src  
typ  
txt  
par  
pid  
st   
234  lemma ne_neg_self {n : ℕ+} (hn1 : (n : ℕ) % 2 = 1) {a : zmod n} (ha : a ≠ 0) : a ≠ -a :=
id                          └┘                           └──┘                  
src                         └┘                            └──┘                     
typ                         └┘                           └──┘                  
doc                         └┘
235  λ h, have a.val ≤ n / 2 ↔ (n : ℕ) / 2 < (-a).val := le_div_two_iff_lt_neg hn1 ha,
id            └──┘                   └─┘     └───────────────────┘ └─┘ └┘
src             └──┘                      └─┘     └───────────────────┘
typ           └──┘                   └─┘     └───────────────────┘ └─┘ └┘
236  by rwa [← h, ← not_lt, not_iff_self] at this
id                 └────┘  └──────────┘
src     └─────┘ └──┘└────┘└┘└──────────┘└─────────
typ     └─────┘└──┘└────┘└┘└──────────┘└─────────
doc     └─────┘ └──┘      └┘            └─────────
txt     └─────┘ └──┘      └┘            └─────────
par     └─────┘ └──┘      └┘            └─────────
pid        └──┘ └──┘      └┘            └──────┘
st     └───────┘└────────┘└────────────┘└────────
237  
src  
typ  
doc  
txt  
par  
pid  
st   
238  @[simp] lemma cast_mul_right_val_cast {n m : ℕ+} (a : ℕ) :
id                                                └┘       
src                                               └┘       
typ                                               └┘       
doc    └──┘                                       └┘
239    ((a : zmod (m * n)).val : zmod m) = (a : zmod m) :=
id          └──┘      └─┘    └──┘        └──┘ 
src          └──┘        └─┘    └──┘          └──┘
typ         └──┘      └─┘    └──┘        └──┘ 
240  zmod.eq_iff_modeq_nat.2 (by rw zmod.val_cast_nat;
id   └───────────────────┘         └───────────────┘
src  └───────────────────┘      └─┘└───────────────┘
typ  └───────────────────┘      └─┘└───────────────┘
doc                              └─┘
txt                              └─┘
par                              └─┘
pid                                
st                              └──────────────────────
241    exact nat.modeq.modeq_of_modeq_mul_right _ (nat.mod_mod _ _))
id           └────────────────────────────────┘    └─────────┘
src    └────┘└────────────────────────────────┘└─┘ └─────────┘└───┘
typ    └────┘└────────────────────────────────┘└─┘ └─────────┘└───┘
doc    └────┘                                  └─┘            └───┘
txt    └────┘                                  └─┘            └───┘
par    └────┘                                  └─┘            └───┘
pid                                           └─┘            └───┘
st   ─────────────────────────────────────────────────────────────┘
242  
243  @[simp] lemma cast_mul_left_val_cast {n m : ℕ+} (a : ℕ) :
id                                               └┘       
src                                              └┘       
typ                                              └┘       
doc    └──┘                                      └┘
244    ((a : zmod (n * m)).val : zmod m) = (a : zmod m) :=
id          └──┘      └─┘    └──┘        └──┘ 
src          └──┘        └─┘    └──┘          └──┘
typ         └──┘      └─┘    └──┘        └──┘ 
245  zmod.eq_iff_modeq_nat.2 (by rw zmod.val_cast_nat;
id   └───────────────────┘         └───────────────┘
src  └───────────────────┘      └─┘└───────────────┘
typ  └───────────────────┘      └─┘└───────────────┘
doc                              └─┘
txt                              └─┘
par                              └─┘
pid                                
st                              └──────────────────────
246    exact nat.modeq.modeq_of_modeq_mul_left _ (nat.mod_mod _ _))
id           └───────────────────────────────┘    └─────────┘
src    └────┘└───────────────────────────────┘└─┘ └─────────┘└───┘
typ    └────┘└───────────────────────────────┘└─┘ └─────────┘└───┘
doc    └────┘                                 └─┘            └───┘
txt    └────┘                                 └─┘            └───┘
par    └────┘                                 └─┘            └───┘
pid                                          └─┘            └───┘
st   ────────────────────────────────────────────────────────────┘
247  
248  lemma cast_val_cast_of_dvd {n m : ℕ+} (h : (m : ℕ) ∣ n) (a : ℕ) :
id                                     └┘                     
src                                    └┘                       
typ                                    └┘                     
doc                                    └┘
249    ((a : zmod n).val : zmod m) = (a : zmod m) :=
id          └──┘  └─┘    └──┘        └──┘ 
src          └──┘   └─┘    └──┘          └──┘
typ         └──┘  └─┘    └──┘        └──┘ 
250  let ⟨k , hk⟩ := h in
id   └─┘            
typ  └─┘            
251  zmod.eq_iff_modeq_nat.2 (nat.modeq.modeq_of_modeq_mul_right k
id   └───────────────────┘   └────────────────────────────────┘
src  └───────────────────┘   └────────────────────────────────┘
typ  └───────────────────┘   └────────────────────────────────┘
252      (by rw [← hk, zmod.val_cast_nat]; exact nat.mod_mod _ _))
id                 └┘  └───────────────┘         └─────────┘
src          └────┘  └┘└───────────────┘  └────┘└─────────┘└──┘
typ          └────┘└┘└┘└───────────────┘  └────┘└─────────┘└──┘
doc          └────┘  └┘                   └────┘           └──┘
txt          └────┘  └┘                   └────┘           └──┘
par          └────┘  └┘                   └────┘           └──┘
pid            └──┘  └┘                                   └──┘
st          └───────┘└─────────────────┘└─────────────────────┘
253  
254  def units_equiv_coprime {n : ℕ+} : units (zmod n) ≃ {x : zmod n // nat.coprime x.1 n} :=
id                                └┘    └───┘  └──┘        └──┘     └─────────┘   
src                               └┘    └───┘  └──┘         └──┘      └─────────┘  
typ                               └┘    └───┘  └──┘        └──┘     └─────────┘   
doc                               └┘                   
255  { to_fun := λ x, ⟨x, nat.modeq.coprime_of_mul_modeq_one (x⁻¹).1.1 begin
id                      └────────────────────────────────┘  └┘  
src                       └────────────────────────────────┘   └┘  
typ                     └────────────────────────────────┘  └┘  
st                                                                     └─────
256      have := units.ext_iff.1 (mul_right_inv x),
id               └───────────┘    └───────────┘ 
src      └──────┘└───────────┘└─┘ └───────────┘ 
typ      └──────┘└───────────┘└─┘ └───────────┘
doc      └──────┘             └─┘               
txt      └──────┘             └─┘               
par      └──────┘             └─┘               
pid      └───┘└─┘             └─┘               
st   ────────────────────────────────────────────┘└─
257      rwa [← zmod.cast_val ((1 : units (zmod n)) : zmod n), units.coe_one, zmod.one_val,
id              └───────────┘       └───┘  └──┘               └───────────┘  └──────────┘
src      └─────┘└───────────┘  └──┘└───┘ └──┘ └───┘     └─┘└───────────┘└┘└──────────┘└─
typ      └─────┘└───────────┘  └──┘└───┘ └──┘└───┘     └─┘└───────────┘└┘└──────────┘└─
doc      └─────┘               └──┘           └───┘     └─┘             └┘            └─
txt      └─────┘               └──┘           └───┘     └─┘             └┘            └─
par      └─────┘               └──┘           └───┘     └─┘             └┘            └─
pid         └──┘               └──┘           └───┘     └─┘             └┘            └─
st   ───────────────────────────────────────────────────────┘└─────────────┘└────────────┘└─
258        ← zmod.cast_val ((x * x⁻¹ : units (zmod n)) : zmod n),
id           └───────────┘      └┘   └───┘  └──┘ 
src  ───────┘└───────────┘    └┘└─┘└───┘ └──┘ └───┘     └──
typ  ───────┘└───────────┘   └┘└─┘└───┘ └──┘└───┘     └──
doc  ───────┘                    └─┘           └───┘     └──
txt  ───────┘                    └─┘           └───┘     └──
par  ───────┘                    └─┘           └───┘     └──
pid  ───────┘                    └─┘           └───┘     └──
st   ──────────────────────────────────────────────────────────┘└─
259        units.coe_mul, zmod.mul_val, zmod.cast_mod_nat, zmod.cast_mod_nat,
id         └───────────┘  └──────────┘  └───────────────┘  └───────────────┘
src  ─────┘└───────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────────┘└─
typ  ─────┘└───────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────────┘└─
doc  ─────┘             └┘            └┘                 └┘                 └─
txt  ─────┘             └┘            └┘                 └┘                 └─
par  ─────┘             └┘            └┘                 └┘                 └─
pid  ─────┘             └┘            └┘                 └┘                 └─
st   ──────────────────┘└────────────┘└─────────────────┘└─────────────────┘└─
260        zmod.eq_iff_modeq_nat] at this
id         └───────────────────┘
src  ─────┘└───────────────────┘└─────────
typ  ─────┘└───────────────────┘└─────────
doc  ─────┘                     └─────────
txt  ─────┘                     └─────────
par  ─────┘                     └─────────
pid  ─────┘                     └──────┘
st   ──────────────────────────┘└────────
261      end⟩,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
262    inv_fun := λ x,
id                  
typ                 
263      have x.val * ↑(gcd_a ((x.val).val) ↑n) = 1,
id            └──┘   └───┘   └──┘ └─┘     
src            └──┘   └───┘    └──┘ └─┘      
typ           └──┘   └───┘   └──┘ └─┘     
doc                     └───┘
264        by rw [← zmod.cast_val x.1, ← int.cast_coe_nat, ← int.cast_one, ← int.cast_mul,
id                  └───────────┘       └──────────────┘    └──────────┘    └──────────┘
src           └────┘└───────────┘ └────┘└──────────────┘└──┘└──────────┘└──┘└──────────┘└─
typ           └────┘└───────────┘└────┘└──────────────┘└──┘└──────────┘└──┘└──────────┘└─
doc           └────┘              └────┘                └──┘            └──┘            └─
txt           └────┘              └────┘                └──┘            └──┘            └─
par           └────┘              └────┘                └──┘            └──┘            └─
pid             └──┘              └────┘                └──┘            └──┘            └─
st           └────────────────────┘└────────────────────┘└──────────────┘└──────────────┘└─
265            zmod.eq_iff_modeq_int, ← int.coe_nat_one, ← (show nat.gcd _ _ = _, from x.2)];
id             └───────────────────┘    └─────────────┘          └─────┘              
src  ─────────┘└───────────────────┘└──┘└─────────────┘└──┘     └─────┘└───┘└───────┘ └──┘
typ  ─────────┘└───────────────────┘└──┘└─────────────┘└──┘     └─────┘└───┘└───────┘└──┘
doc  ─────────┘                     └──┘               └──┘            └───┘ └───────┘ └──┘
txt  ─────────┘                     └──┘               └──┘            └───┘ └───────┘ └──┘
par  ─────────┘                     └──┘               └──┘            └───┘ └───────┘ └──┘
pid  ─────────┘                     └──┘               └──┘            └───┘ └───────┘ └──┘
st   ──────────────────────────────┘└─────────────────┘└──────────────────────────────────┘└─
266          simpa using int.modeq.gcd_a_modeq x.1.1 n,
id                       └───────────────────┘      
src          └──────────┘└───────────────────┘ └───┘
typ          └──────────┘└───────────────────┘└───┘
doc          └──────────┘                      └───┘
txt          └──────────┘                      └───┘
par          └──────────┘                      └───┘
pid               └────┘                      └───┘
st   ────────────────────────────────────────────────┘
267      ⟨x.1, gcd_a x.1.1 n, this, by simpa [mul_comm] using this⟩,
id           └───┘      └──┘            └──────┘        └──┘
src           └───┘                 └─────┘└──────┘└──────┘
typ          └───┘      └──┘     └─────┘└──────┘└──────┘└──┘
doc            └───┘                   └─────┘        └──────┘
txt                                    └─────┘        └──────┘
par                                    └─────┘        └──────┘
pid                                                 └────┘
st                                    └──────────────────────────┘
268    left_inv := λ ⟨_, _, _, _⟩, units.ext rfl,
id                                └───────┘ └─┘
src                                └───────┘ └─┘
typ                               └───────┘ └─┘
269    right_inv := λ ⟨_, _⟩, rfl }
id                           └─┘
src                           └─┘
typ                          └─┘
270  
271  /-- `val_min_abs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
272    The result will be in the interval `(-n/2, n/2]` -/
273  def val_min_abs {n : ℕ+} (x : zmod n) : ℤ :=
id                        └┘       └──┘     
src                       └┘       └──┘      
typ                       └┘       └──┘     
doc                       └┘
274  if x.val ≤ n / 2 then x.val else x.val - n
id      └──┘           └──┘      └──┘  
src      └──┘             └──┘       └──┘ 
typ     └──┘           └──┘      └──┘  
275  
276  @[simp] lemma coe_val_min_abs {n : ℕ+} (x : zmod n) :
id                                      └┘       └──┘ 
src                                     └┘       └──┘
typ                                     └┘       └──┘ 
doc    └──┘                             └┘
277    (x.val_min_abs : zmod n) = x :=
id      └──────────┘   └──┘    
src      └──────────┘   └──┘    
typ     └──────────┘   └──┘    
doc      └──────────┘
278  by simp [zmod.val_min_abs]; split_ifs; simp
id            └──────────────┘
src     └────┘└──────────────┘  └───────┘  └────
typ     └────┘└──────────────┘  └───────┘  └────
doc     └────┘└──────────────┘  └───────┘  └────
txt     └────┘                  └───────┘  └────
par     └────┘                  └───────┘  └────
pid                                          
st     └─────────────────────────────────────────
279  
src  
typ  
doc  
txt  
par  
pid  
st   
280  lemma nat_abs_val_min_abs_le {n : ℕ+} (x : zmod n) : x.val_min_abs.nat_abs ≤ n / 2 :=
id                                     └┘       └──┘     └──────────┘└──────┘   
src                                    └┘       └──┘       └──────────┘└──────┘    
typ                                    └┘       └──┘     └──────────┘└──────┘   
doc                                    └┘                  └──────────┘
281  have (x.val - n : ℤ) ≤ 0, from sub_nonpos.2 $ int.coe_nat_le.2 $ le_of_lt x.2,
id         └──┘                └────────┘    └────────────┘    └──────┘ 
src         └──┘                 └────────┘    └────────────┘    └──────┘  
typ        └──┘                └────────┘    └────────────┘    └──────┘ 
282  begin
st   └─────
283    rw zmod.val_min_abs,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘└──────────────┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
284    split_ifs with h,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid             └────┘
st   ─────────────────┘└─
285    { exact h },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
286    { rw [← int.coe_nat_le, int.of_nat_nat_abs_of_nonpos this, neg_sub],
id             └────────────┘  └──────────────────────────┘ └──┘  └─────┘
src      └────┘└────────────┘└┘└──────────────────────────┘    └┘└─────┘
typ      └────┘└────────────┘└┘└──────────────────────────┘└──┘└┘└─────┘
doc      └────┘              └┘                                └┘       
txt      └────┘              └┘                                └┘       
par      └────┘              └┘                                └┘       
pid        └──┘              └┘                                └┘       
st   ───────────────────────┘└─────────────────────────────────┘└───────┘└──
287      conv_lhs { congr, rw [coe_coe, ← nat.mod_add_div n 2, int.coe_nat_add, int.coe_nat_mul,
id                             └─────┘    └─────────────┘     └─────────────┘  └─────────────┘
src      └─────────┘└───┘└┘└──┘└─────┘└──┘└─────────────┘ └──┘└─────────────┘└┘└─────────────┘└─
typ      └─────────┘└───┘└┘└──┘└─────┘└──┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘└─
doc                            └─────┘
txt      └─────────┘└───┘└┘└──┘       └──┘                └──┘               └┘               └─
par      └─────────┘└───┘└┘└──┘       └──┘                └──┘               └┘               └─
pid              └───────────┘       └──┘                └──┘               └┘               └─
st   ─────────────┘└────┘└───────────┘└────────────────────┘└────────────────┘└───────────────┘└─
288        int.coe_nat_bit0, int.coe_nat_one] },
id         └──────────────┘  └─────────────┘
src  ─────┘└──────────────┘└┘└─────────────┘└┘
typ  ─────┘└──────────────┘└┘└─────────────┘└┘
txt  ─────┘                └┘               └┘
par  ─────┘                └┘               └┘
pid  ─────┘                └┘               └─┘
st   ─────────────────────┘└───────────────┘ └┘
289      rw ← sub_nonneg,
id            └────────┘
src      └───┘└────────┘
typ      └───┘└────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ──────────────────┘└─
290      suffices : (0 : ℤ) ≤ x.val - ((n % 2 : ℕ) + (n / 2 : ℕ)),
id                           └───┘                 
src      └─────────┘ └──┘ └┘└───┘   └───┘ └┘  └───┘ └┘
typ      └─────────┘ └──┘ └┘└───┘   └───┘ └┘ └───┘ └┘
doc      └─────────┘ └──┘ └┘           └───┘ └┘    └───┘ └┘
txt      └─────────┘ └──┘ └┘           └───┘ └┘    └───┘ └┘
par      └─────────┘ └──┘ └┘           └───┘ └┘    └───┘ └┘
pid      └───────┘└┘ └──┘ └┘           └───┘ └┘    └───┘ └┘
st   ───────────────────────────────────────────────────────────┘└─
291      { exact le_trans this (le_of_eq $ by ring) },
id               └──────┘ └──┘  └──────┘
src        └────┘└──────┘     └──────┘   └──┘└┘
typ        └────┘└──────┘└──┘ └──────┘   └──┘└┘
doc        └────┘                        └──┘└┘
txt        └────┘                        └──┘└┘
par        └────┘                        └──┘└┘
pid                                     └────┘
st   ─────┘└────────────────────────────────┘└───┘└┘└┘
292      exact sub_nonneg.2 (by rw [← int.coe_nat_add, int.coe_nat_le];
id             └────────┘             └─────────────┘  └────────────┘
src      └────┘└────────┘└─┘   └────┘└─────────────┘└┘└────────────┘└─
typ      └────┘└────────┘└─┘   └────┘└─────────────┘└┘└────────────┘└─
doc      └────┘          └─┘   └────┘               └┘              └─
txt      └────┘          └─┘   └────┘               └┘              └─
par      └────┘          └─┘   └────┘               └┘              └─
pid                     └─┘   └─────┘               └┘              └──
st   ─────────────────────────┘└────────────────────┘└──────────────┘└─
293        exact calc (n : ℕ) % 2 + n / 2 ≤ 1 + n / 2 :
id                                              
src  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘   └────
typ  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘  └────
doc  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘   └────
txt  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘   └────
par  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘   └────
pid  ───────────┘      └─┘ └┘ └─┘   └─┘ └─┘   └────
st   ───────────────────────────────────────────────────
294          add_le_add (nat.le_of_lt_succ (nat.mod_lt _ dec_trivial)) (le_refl _)
id           └────────┘  └───────────────┘  └────────┘   └─────────┘    └─────┘
src  ───────┘└────────┘ └───────────────┘ └────────┘└─┘└─────────┘└─┘ └─────┘└───
typ  ───────┘└────────┘ └───────────────┘ └────────┘└─┘└─────────┘└─┘ └─────┘└───
doc  ───────┘                                       └─┘└─────────┘└─┘        └───
txt  ───────┘                                       └─┘           └─┘        └───
par  ───────┘                                       └─┘           └─┘        └───
pid  ───────┘                                       └─┘           └─┘        └───
st   ──────────────────────────────────────────────────────────────────────────────
295          ... ≤ x.val : by rw add_comm; exact nat.succ_le_of_lt (lt_of_not_ge h)) }
id                 └───┘         └──────┘        └───────────────┘  └──────────┘ 
src  ───────────┘ └───┘└─┘  └─┘└──────┘└──────┘└───────────────┘ └──────────┘ └─┘
typ  ───────────┘ └───┘└─┘  └─┘└──────┘└──────┘└───────────────┘ └──────────┘└─┘
doc  ───────────┘      └─┘  └─┘        └──────┘                               └─┘
txt  ───────────┘      └─┘  └─┘        └──────┘                               └─┘
par  ───────────┘      └─┘  └─┘        └──────┘                               └─┘
pid  ───────────┘      └─┘  └──┘        └──────┘                               └┘
st   ───────────────────────┘└────────────────────────────────────────────────────┘└┘└─
296  end
st   ──┘
297  
298  @[simp] lemma val_min_abs_zero {n : ℕ+} : (0 : zmod n).val_min_abs = 0 :=
id                                       └┘         └──┘  └─────────┘  
src                                      └┘         └──┘   └─────────┘  
typ                                      └┘         └──┘  └─────────┘  
doc    └──┘                              └┘                └─────────┘
299  by simp [zmod.val_min_abs]
id            └──────────────┘
src     └────┘└──────────────┘└─
typ     └────┘└──────────────┘└─
doc     └────┘└──────────────┘└─
txt     └────┘                └─
par     └────┘                └─
pid                         
st     └────────────────────────
300  
src  
typ  
doc  
txt  
par  
pid  
st   
301  @[simp] lemma val_min_abs_eq_zero {n : ℕ+} (x : zmod n) :
id                                          └┘       └──┘ 
src                                         └┘       └──┘
typ                                         └┘       └──┘ 
doc    └──┘                                 └┘
302    x.val_min_abs = 0 ↔ x = 0 :=
id     └──────────┘      
src     └──────────┘       
typ    └──────────┘      
doc     └──────────┘
303  ⟨λ h, begin
id      
typ     
st         └─────
304    dsimp [zmod.val_min_abs] at h,
id            └──────────────┘
src    └─────┘└──────────────┘└────┘
typ    └─────┘└──────────────┘└────┘
doc    └─────┘└──────────────┘└────┘
txt    └─────┘                └────┘
par    └─────┘                └────┘
pid                         └──┘
st   ──────────────────────────────┘└─
305    split_ifs at h,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid             └───┘
st   ───────────────┘└─
306    { exact fin.eq_of_veq (by simp * at *) },
id             └───────────┘
src      └────┘└───────────┘   └─────────┘└┘
typ      └────┘└───────────┘   └─────────┘└┘
doc      └────┘                └─────────┘└┘
txt      └────┘                └─────────┘└┘
par      └────┘                └─────────┘└┘
pid                           └───────────┘
st   ───┘└─────────────────────┘└──────────┘└┘└┘
307    { exact absurd h (mt sub_eq_zero.1 (ne_of_lt $ int.coe_nat_lt.2 x.2)) }
id             └────┘   └┘ └─────────┘    └──────┘   └────────────┘   
src      └────┘└────┘  └┘└─────────┘└─┘ └──────┘ └────────────┘└─┘ └───┘
typ      └────┘└────┘ └┘└─────────┘└─┘ └──────┘ └────────────┘└─┘└───┘
doc      └────┘                     └─┘                        └─┘ └───┘
txt      └────┘                     └─┘                        └─┘ └───┘
par      └────┘                     └─┘                        └─┘ └───┘
pid                                └─┘                        └─┘ └──┘
st   ───────────────────────────────────────────────────────────────────────┘└─
308  end, λ hx0, hx0.symm ▸ zmod.val_min_abs_zero⟩
id          └─┘  └─┘└───┘  └───────────────────┘
src                 └───┘  └───────────────────┘
typ         └─┘  └─┘└───┘  └───────────────────┘
st   ──┘
309  
310  lemma cast_nat_abs_val_min_abs {n : ℕ+} (a : zmod n) :
id                                       └┘       └──┘ 
src                                      └┘       └──┘
typ                                      └┘       └──┘ 
doc                                      └┘
311    (a.val_min_abs.nat_abs : zmod n) = if a.val ≤ (n : ℕ) / 2 then a else -a :=
id      └──────────┘└──────┘   └──┘       └──┘                      
src      └──────────┘└──────┘   └──┘         └──┘                        
typ     └──────────┘└──────┘   └──┘       └──┘                      
doc      └──────────┘
312  have (a.val : ℤ) + -n ≤ 0, by erw [sub_nonpos, int.coe_nat_le]; exact le_of_lt a.2,
id         └──┘                   └────────┘  └────────────┘         └──────┘ 
src         └──┘               └───┘└────────┘└┘└────────────┘  └────┘└──────┘ └┘
typ        └──┘              └───┘└────────┘└┘└────────────┘  └────┘└──────┘└┘
doc                                └───┘          └┘                └────┘         └┘
txt                                └───┘          └┘                └────┘         └┘
par                                └───┘          └┘                └────┘         └┘
pid                                   └┘          └┘                              └┘
st                                └──────────────┘└──────────────┘└──────────────────┘
313  begin
st   └─────
314    dsimp [zmod.val_min_abs],
id            └──────────────┘
src    └─────┘└──────────────┘
typ    └─────┘└──────────────┘
doc    └─────┘└──────────────┘
txt    └─────┘                
par    └─────┘                
pid                         
st   ─────────────────────────┘└─
315    split_ifs,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
316    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
317    { erw [← int.cast_coe_nat, int.of_nat_nat_abs_of_nonpos this],
id              └──────────────┘  └──────────────────────────┘ └──┘
src      └─────┘└──────────────┘└┘└──────────────────────────┘    
typ      └─────┘└──────────────┘└┘└──────────────────────────┘└──┘
doc      └─────┘                └┘                                
txt      └─────┘                └┘                                
par      └─────┘                └┘                                
pid         └──┘                └┘                                
st   ──────────────────────────┘└─────────────────────────────────┘└──
318      simp }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
319  end
st   ──┘
320  
321  @[simp] lemma nat_abs_val_min_abs_neg {n : ℕ+} (a : zmod n) :
id                                              └┘       └──┘ 
src                                             └┘       └──┘
typ                                             └┘       └──┘ 
doc    └──┘                                     └┘
322    (-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs :=
id       └─────────┘ └─────┘   └──────────┘└──────┘
src       └─────────┘ └─────┘    └──────────┘└──────┘
typ      └─────────┘ └─────┘   └──────────┘└──────┘
doc        └─────────┘             └──────────┘
323  if haa : -a = a then by rw [haa]
id   └┘                      └─┘
src  └┘                    └──┘   └┘
typ  └┘                  └──┘└─┘└┘
doc                          └──┘   └┘
txt                          └──┘   └┘
par                          └──┘   └┘
pid                            └┘   
st                          └──────┘
324  else
325  have hpa : (n : ℕ) - a.val ≤ n / 2 ↔ (n : ℕ) / 2 < a.val,
id   └──┘              └──┘                 └──┘
src  └──┘                └──┘                    └──┘
typ  └──┘              └──┘                 └──┘
326    from suffices (((n : ℕ) % 2) + 2 * (n / 2)) - a.val ≤ (n : ℕ) / 2 ↔ (n : ℕ) / 2 < a.val,
id                                           └──┘                      └──┘
src                                             └──┘                         └──┘
typ                                          └──┘                      └──┘
327      by rwa [nat.mod_add_div] at this,
id               └─────────────┘
src         └───┘└─────────────┘└───────┘
typ         └───┘└─────────────┘└───────┘
doc         └───┘               └───────┘
txt         └───┘               └───────┘
par         └───┘               └───────┘
pid            └┘               └──────┘
st         └───────────────────┘└──────┘
328    begin
st     └─────
329      rw [nat.sub_le_iff, two_mul, ← add_assoc, nat.add_sub_cancel],
id           └────────────┘  └─────┘    └───────┘  └────────────────┘
src      └──┘└────────────┘└┘└─────┘└──┘└───────┘└┘└────────────────┘
typ      └──┘└────────────┘└┘└─────┘└──┘└───────┘└┘└────────────────┘
doc      └──┘              └┘       └──┘         └┘                  
txt      └──┘              └┘       └──┘         └┘                  
par      └──┘              └┘       └──┘         └┘                  
pid        └┘              └┘       └──┘         └┘                  
st   ─────────────────────┘└───────┘└───────────┘└──────────────────┘└──
330      cases (n : ℕ).mod_two_eq_zero_or_one with hn0 hn1,
id              
src      └────┘  └─┘ └───────────────────────────────────┘
typ      └────┘ └─┘ └───────────────────────────────────┘
doc      └────┘  └─┘ └───────────────────────────────────┘
txt      └────┘  └─┘ └───────────────────────────────────┘
par      └────┘  └─┘ └───────────────────────────────────┘
pid             └─┘ └─────────────────────┘└────────────┘
st   ────────────────────────────────────────────────────┘└─
331      { split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ─────┘└───┘└─
332        { exact λ h, lt_of_le_of_ne (le_trans (nat.le_add_left _ _) h)
id                      └────────────┘  └──────┘  └─────────────┘
src          └────┘ └──┘└────────────┘ └──────┘ └─────────────┘└────┘ └─
typ          └────┘ └──┘└────────────┘ └──────┘ └─────────────┘└────┘ └─
doc          └────┘ └──┘                                       └────┘ └─
txt          └────┘ └──┘                                       └────┘ └─
par          └────┘ └──┘                                       └────┘ └─
pid                └──┘                                       └────┘ └─
st   ───────┘└────────────────────────────────────────────────────────────
333            begin
src  ─────────┘     
typ  ─────────┘     
doc  ─────────┘     
txt  ─────────┘     
par  ─────────┘     
pid  ─────────┘     
st   ─────────┘└─────
334              assume hna,
src  ───────────┘└────────┘└─
typ  ───────────┘└────────┘└─
doc  ───────────┘└────────┘└─
txt  ───────────┘└────────┘└─
par  ───────────┘└────────┘└─
pid  ────────────────────────
st   ─────────────────────┘└─
335              rw [← zmod.cast_val a, ← hna, neg_eq_iff_add_eq_zero, ← nat.cast_add,
id                     └───────────┘     └─┘  └────────────────────┘    └──────────┘
src  ───────────┘└────┘└───────────┘ └──┘   └┘└────────────────────┘└──┘└──────────┘└─
typ  ───────────┘└────┘└───────────┘└──┘└─┘└┘└────────────────────┘└──┘└──────────┘└─
doc  ───────────┘└────┘              └──┘   └┘                      └──┘            └─
txt  ───────────┘└────┘              └──┘   └┘                      └──┘            └─
par  ───────────┘└────┘              └──┘   └┘                      └──┘            └─
pid  ─────────────────┘              └──┘   └┘                      └──┘            └─
st   ────────────────────────────────┘└─────┘└──────────────────────┘└──────────────┘└─
336                zmod.eq_zero_iff_dvd_nat, ← two_mul, ← zero_add (2 * _), ← hn0,
id                 └──────────────────────┘    └─────┘    └──────┘           └─┘
src  ─────────────┘└──────────────────────┘└──┘└─────┘└──┘└──────┘ └┘└─────┘   └─
typ  ─────────────┘└──────────────────────┘└──┘└─────┘└──┘└──────┘ └┘└─────┘└─┘└─
doc  ─────────────┘                        └──┘       └──┘         └┘ └─────┘   └─
txt  ─────────────┘                        └──┘       └──┘         └┘ └─────┘   └─
par  ─────────────┘                        └──┘       └──┘         └┘ └─────┘   └─
pid  ─────────────┘                        └──┘       └──┘         └┘ └─────┘   └─
st   ─────────────────────────────────────┘└─────────┘└──────────────────┘└─────┘└─
337                nat.mod_add_div] at haa,
id                 └─────────────┘
src  ─────────────┘└─────────────┘└──────┘└─
typ  ─────────────┘└─────────────┘└──────┘└─
doc  ─────────────┘               └──────┘└─
txt  ─────────────┘               └──────┘└─
par  ─────────────┘               └──────┘└─
pid  ─────────────┘               └─────────
st   ────────────────────────────┘└─────┘└─
338              exact haa (dvd_refl _)
id                     └─┘  └──────┘
src  ─────────────────┘    └──────┘└───
typ  ─────────────────┘└─┘ └──────┘└───
doc  ─────────────────┘            └───
txt  ─────────────────┘            └───
par  ─────────────────┘            └───
pid  ─────────────────┘            └───
st   ───────────────────────────────────
339            end },
src  ─────────────┘
typ  ─────────────┘
doc  ─────────────┘
txt  ─────────────┘
par  ─────────────┘
pid  ────────────┘
st   ─────────┘└─┘└┘
340        { rw [hn0, zero_add], exact le_of_lt } },
id               └─┘  └──────┘         └──────┘
src          └──┘   └┘└──────┘  └────┘└──────┘
typ          └──┘└─┘└┘└──────┘  └────┘└──────┘
doc          └──┘   └┘          └────┘        
txt          └──┘   └┘          └────┘        
par          └──┘   └┘          └────┘        
pid            └┘   └┘                       
st   ──────────────┘└────────┘└────────────────┘└──┘
341      { rw [hn1, add_comm, nat.succ_le_iff] }
id             └─┘  └──────┘  └─────────────┘
src        └──┘   └┘└──────┘└┘└─────────────┘└┘
typ        └──┘└─┘└┘└──────┘└┘└─────────────┘└┘
doc        └──┘   └┘        └┘               └┘
txt        └──┘   └┘        └┘               └┘
par        └──┘   └┘        └┘               └┘
pid          └┘   └┘        └┘               
st   ────────────┘└────────┘└───────────────┘└─
342    end,
st   ────┘
343  have ha0 : ¬ a = 0, from λ ha0, by simp * at *,
id                           └─┘
src                                   └─────────┘
typ                          └─┘     └─────────┘
doc                                     └─────────┘
txt                                     └─────────┘
par                                     └─────────┘
pid                                         └──┘
st                                     └──────────┘
344  begin
st   └─────
345    dsimp [zmod.val_min_abs],
id            └──────────────┘
src    └─────┘└──────────────┘
typ    └─────┘└──────────────┘
doc    └─────┘└──────────────┘
txt    └─────┘                
par    └─────┘                
pid                         
st   ─────────────────────────┘└─
346    rw [← not_le] at hpa,
id           └────┘
src    └────┘└────┘└──────┘
typ    └────┘└────┘└──────┘
doc    └────┘      └──────┘
txt    └────┘      └──────┘
par    └────┘      └──────┘
pid      └──┘      └─────┘
st   ─────────────┘└─────┘└─
347    simp only [if_neg ha0, zmod.neg_val, hpa, int.coe_nat_sub (le_of_lt a.2)],
id                └────┘ └─┘  └──────────┘  └─┘  └─────────────┘  └──────┘ 
src    └─────────┘└────┘   └┘└──────────┘└┘   └┘└─────────────┘ └──────┘ └──┘
typ    └─────────┘└────┘└─┘└┘└──────────┘└┘└─┘└┘└─────────────┘ └──────┘└──┘
doc    └─────────┘         └┘            └┘   └┘                         └──┘
txt    └─────────┘         └┘            └┘   └┘                         └──┘
par    └─────────┘         └┘            └┘   └┘                         └──┘
pid        └──┘└┘         └┘            └┘   └┘                         └──┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
348    split_ifs,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
349    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
350    { rw [← int.nat_abs_neg], simp }
id             └─────────────┘
src      └────┘└─────────────┘  └───┘
typ      └────┘└─────────────┘  └───┘
doc      └────┘                 └───┘
txt      └────┘                 └───┘
par      └────┘                 └───┘
pid        └──┘                     
st   ────────────────────────┘└──────┘└─
351  end
st   ──┘
352  
353  lemma val_eq_ite_val_min_abs {n : ℕ+} (a : zmod n) :
id                                     └┘       └──┘ 
src                                    └┘       └──┘
typ                                    └┘       └──┘ 
doc                                    └┘
354    (a.val : ℤ) = a.val_min_abs + if a.val ≤ n / 2 then 0 else n :=
id      └──┘      └──────────┘     └──┘                  
src      └──┘       └──────────┘      └──┘    
typ     └──┘      └──────────┘     └──┘                  
doc                   └──────────┘
355  by simp [zmod.val_min_abs]; split_ifs; simp
id            └──────────────┘
src     └────┘└──────────────┘  └───────┘  └────
typ     └────┘└──────────────┘  └───────┘  └────
doc     └────┘└──────────────┘  └───────┘  └────
txt     └────┘                  └───────┘  └────
par     └────┘                  └───────┘  └────
pid                                          
st     └─────────────────────────────────────────
356  
src  
typ  
doc  
txt  
par  
pid  
st   
357  lemma neg_eq_self_mod_two : ∀ (a : zmod 2), -a = a := dec_trivial
id                                      └──┘           └─────────┘
src                                     └──┘             └─────────┘
typ                                     └──┘           └─────────┘
doc                                                        └─────────┘
358  
359  @[simp] lemma nat_abs_mod_two (a : ℤ) : (a.nat_abs : zmod 2) = a :=
id                                           └──────┘   └──┘     
src                                           └──────┘   └──┘    
typ                                          └──────┘   └──┘     
doc    └──┘
360  by cases a; simp [zmod.neg_eq_self_mod_two]
id                    └──────────────────────┘
src     └────┘   └────┘└──────────────────────┘└─
typ     └────┘  └────┘└──────────────────────┘└─
doc     └────┘   └────┘                        └─
txt     └────┘   └────┘                        └─
par     └────┘   └────┘                        └─
pid                                         
st     └─────────────────────────────────────────
361  
src  
typ  
doc  
txt  
par  
pid  
st   
362  section
363  variables {α : Type*} [has_zero α] [has_one α] [has_add α] {n : ℕ+}
id                          └──────┘     └─────┘     └─────┘         └┘
src                         └──────┘     └─────┘     └─────┘         └┘
typ                         └──────┘     └─────┘     └─────┘         └┘
doc                                                                  └┘
364  
365  def cast : zmod n → α := nat.cast ∘ fin.val
id              └──┘        └──────┘  └─────┘
src             └──┘          └──────┘  └─────┘
typ             └──┘        └──────┘  └─────┘
doc                           └──────┘
366  
367  end
368  
369  end zmod
370  
371  def zmodp (p : ℕ) (hp : prime p) : Type := zmod ⟨p, hp.pos⟩
id                          └───┘             └──┘    └┘└──┘
src                         └───┘              └──┘       └──┘
typ                         └───┘             └──┘    └┘└──┘
doc                          └───┘
372  
373  namespace zmodp
374  
375  variables {p : ℕ} (hp : prime p)
id                          └───┘
src                         └───┘
typ                         └───┘
doc                          └───┘
376  
377  instance : comm_ring (zmodp p hp) := zmod.comm_ring ⟨p, hp.pos⟩
id              └───────┘  └───┘  └┘     └────────────┘    └┘└──┘
src             └───────┘  └───┘          └────────────┘       └──┘
typ             └───────┘  └───┘  └┘     └────────────┘    └┘└──┘
378  
379  instance : inhabited (zmodp p hp) := ⟨0⟩
id              └───────┘  └───┘  └┘
src             └───────┘  └───┘
typ             └───────┘  └───┘  └┘
380  
381  instance {p : ℕ} (hp : prime p) : has_inv (zmodp p hp) :=
id                         └───┘     └─────┘  └───┘  └┘
src                        └───┘      └─────┘  └───┘
typ                        └───┘     └─────┘  └───┘  └┘
doc                         └───┘
382  ⟨λ a, gcd_a a.1 p⟩
id        └───┘   
src        └───┘  
typ       └───┘   
doc        └───┘
383  
384  lemma add_val : ∀ a b : zmodp p hp, (a + b).val = (a.val + b.val) % p
id                          └───┘  └┘      └─┘    └──┘  └──┘   
src                          └───┘             └─┘     └──┘   └──┘  
typ                         └───┘  └┘      └─┘    └──┘  └──┘   
385  | ⟨_, _⟩ ⟨_, _⟩ := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
386  
387  lemma mul_val : ∀ a b : zmodp p hp, (a * b).val = (a.val * b.val) % p
id                          └───┘  └┘      └─┘    └──┘  └──┘   
src                          └───┘             └─┘     └──┘   └──┘  
typ                         └───┘  └┘      └─┘    └──┘  └──┘   
388  | ⟨_, _⟩ ⟨_, _⟩ := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
389  
390  @[simp] lemma one_val : (1 : zmodp p hp).val = 1 :=
id                                └───┘  └┘ └─┘  
src                               └───┘      └─┘  
typ                               └───┘  └┘ └─┘  
doc    └──┘
391  nat.mod_eq_of_lt hp.one_lt
id   └──────────────┘ └┘└─────┘
src  └──────────────┘   └─────┘
typ  └──────────────┘ └┘└─────┘
392  
393  @[simp] lemma zero_val : (0 : zmodp p hp).val = 0 := rfl
id                                 └───┘  └┘ └─┘        └─┘
src                                └───┘      └─┘        └─┘
typ                                └───┘  └┘ └─┘        └─┘
doc    └──┘
394  
395  lemma val_cast_nat (a : ℕ) : (a : zmodp p hp).val = a % p :=
id                                   └───┘  └┘ └─┘     
src                                   └───┘      └─┘     
typ                                  └───┘  └┘ └─┘     
396  @zmod.val_cast_nat ⟨p, hp.pos⟩ _
id    └───────────────┘    └┘└──┘
src   └───────────────┘       └──┘
typ   └───────────────┘    └┘└──┘
397  
398  lemma mk_eq_cast {a : ℕ} (h : a < p) : (⟨a, h⟩ : zmodp p hp) = (a : zmodp p hp) :=
id                                              └───┘  └┘       └───┘  └┘
src                                                 └───┘             └───┘
typ                                             └───┘  └┘       └───┘  └┘
399  @zmod.mk_eq_cast ⟨p, hp.pos⟩ _ _
id    └─────────────┘    └┘└──┘
src   └─────────────┘       └──┘
typ   └─────────────┘    └┘└──┘
400  
401  @[simp] lemma cast_self_eq_zero: (p : zmodp p hp) = 0 :=
id                                        └───┘  └┘  
src                                        └───┘       
typ                                       └───┘  └┘  
doc    └──┘
402  fin.eq_of_veq $ by simp [val_cast_nat]
id   └───────────┘            └──────────┘
src  └───────────┘      └────┘└──────────┘└─
typ  └───────────┘      └────┘└──────────┘└─
doc                     └────┘            └─
txt                     └────┘            └─
par                     └────┘            └─
pid                                     
st                     └────────────────────
403  
src  
typ  
doc  
txt  
par  
pid  
st   
404  lemma val_cast_of_lt {a : ℕ} (h : a < p) : (a : zmodp p hp).val = a :=
id                                              └───┘  └┘ └─┘   
src                                                └───┘      └─┘  
typ                                             └───┘  └┘ └─┘   
405  @zmod.val_cast_of_lt ⟨p, hp.pos⟩ _ h
id    └─────────────────┘    └┘└──┘    
src   └─────────────────┘       └──┘
typ   └─────────────────┘    └┘└──┘    
406  
407  @[simp] lemma cast_mod_nat (a : ℕ) : ((a % p : ℕ) : zmodp p hp) = a :=
id                                                  └───┘  └┘   
src                                                   └───┘       
typ                                                 └───┘  └┘   
doc    └──┘
408  @zmod.cast_mod_nat ⟨p, hp.pos⟩ _
id    └───────────────┘    └┘└──┘
src   └───────────────┘       └──┘
typ   └───────────────┘    └┘└──┘
409  
410  @[simp] lemma cast_val (a : zmodp p hp) : (a.val : zmodp p hp) = a :=
id                               └───┘  └┘     └──┘   └───┘  └┘   
src                              └───┘           └──┘   └───┘       
typ                              └───┘  └┘     └──┘   └───┘  └┘   
doc    └──┘
411  @zmod.cast_val ⟨p, hp.pos⟩ _
id    └───────────┘    └┘└──┘
src   └───────────┘       └──┘
typ   └───────────┘    └┘└──┘
412  
413  @[simp] lemma cast_mod_int (a : ℤ) : ((a % p : ℤ) : zmodp p hp) = a :=
id                                                  └───┘  └┘   
src                                                   └───┘       
typ                                                 └───┘  └┘   
doc    └──┘
414  @zmod.cast_mod_int ⟨p, hp.pos⟩ _
id    └───────────────┘    └┘└──┘
src   └───────────────┘       └──┘
typ   └───────────────┘    └┘└──┘
415  
416  lemma val_cast_int (a : ℤ) : (a : zmodp p hp).val = (a % p).nat_abs :=
id                                   └───┘  └┘ └─┘       └─────┘
src                                   └───┘      └─┘         └─────┘
typ                                  └───┘  └┘ └─┘       └─────┘
417  @zmod.val_cast_int ⟨p, hp.pos⟩ _
id    └───────────────┘    └┘└──┘
src   └───────────────┘       └──┘
typ   └───────────────┘    └┘└──┘
418  
419  lemma coe_val_cast_int  (a : ℤ) : ((a : zmodp p hp).val : ℤ) = a % (p : ℕ) :=
id                                         └───┘  └┘ └─┘             
src                                         └───┘      └─┘               
typ                                        └───┘  └┘ └─┘             
420  @zmod.coe_val_cast_int ⟨p, hp.pos⟩ _
id    └───────────────────┘    └┘└──┘
src   └───────────────────┘       └──┘
typ   └───────────────────┘    └┘└──┘
421  
422  lemma eq_iff_modeq_nat {a b : ℕ} : (a : zmodp p hp) = b ↔ a ≡ b [MOD p] :=
id                                         └───┘  └┘        └──┘ 
src                                         └───┘                └──┘  
typ                                        └───┘  └┘        └──┘ 
doc                                                                 └──┘  
423  @zmod.eq_iff_modeq_nat ⟨p, hp.pos⟩ _ _
id    └───────────────────┘    └┘└──┘
src   └───────────────────┘       └──┘
typ   └───────────────────┘    └┘└──┘
424  
425  lemma eq_iff_modeq_int {a b : ℤ} : (a : zmodp p hp) = b ↔ a ≡ b [ZMOD p] :=
id                                         └───┘  └┘        └───┘ 
src                                         └───┘                └───┘  
typ                                        └───┘  └┘        └───┘ 
426  @zmod.eq_iff_modeq_int ⟨p, hp.pos⟩ _ _
id    └───────────────────┘    └┘└──┘
src   └───────────────────┘       └──┘
typ   └───────────────────┘    └┘└──┘
427  
428  lemma eq_zero_iff_dvd_nat (a : ℕ) : (a : zmodp p hp) = 0 ↔ p ∣ a :=
id                                          └───┘  └┘        
src                                          └───┘             
typ                                         └───┘  └┘        
429  @zmod.eq_zero_iff_dvd_nat ⟨p, hp.pos⟩ _
id    └──────────────────────┘    └┘└──┘
src   └──────────────────────┘       └──┘
typ   └──────────────────────┘    └┘└──┘
430  
431  lemma eq_zero_iff_dvd_int (a : ℤ) : (a : zmodp p hp) = 0 ↔ (p : ℤ) ∣ a :=
id                                          └───┘  └┘             
src                                          └───┘                  
typ                                         └───┘  └┘             
432  @zmod.eq_zero_iff_dvd_int ⟨p, hp.pos⟩ _
id    └──────────────────────┘    └┘└──┘
src   └──────────────────────┘       └──┘
typ   └──────────────────────┘    └┘└──┘
433  
434  instance : fintype (zmodp p hp) := @zmod.fintype ⟨p, hp.pos⟩
id              └─────┘  └───┘  └┘      └──────────┘    └┘└──┘
src             └─────┘  └───┘           └──────────┘       └──┘
typ             └─────┘  └───┘  └┘      └──────────┘    └┘└──┘
doc             └─────┘
435  
436  instance decidable_eq : decidable_eq (zmodp p hp) := fin.decidable_eq _
id                           └──────────┘  └───┘  └┘     └──────────────┘
src                          └──────────┘  └───┘          └──────────────┘
typ                          └──────────┘  └───┘  └┘     └──────────────┘
437  
438  instance : has_repr (zmodp p hp) := fin.has_repr _
id              └──────┘  └───┘  └┘     └──────────┘
src             └──────┘  └───┘          └──────────┘
typ             └──────┘  └───┘  └┘     └──────────┘
439  
440  @[simp] lemma card_zmodp : fintype.card (zmodp p hp) = p :=
id                              └──────────┘  └───┘  └┘   
src                             └──────────┘  └───┘       
typ                             └──────────┘  └───┘  └┘   
doc    └──┘                     └──────────┘
441  @zmod.card_zmod ⟨p, hp.pos⟩
id    └────────────┘    └┘└──┘
src   └────────────┘       └──┘
typ   └────────────┘    └┘└──┘
442  
443  lemma le_div_two_iff_lt_neg {p : ℕ} (hp : prime p) (hp1 : p % 2 = 1)
id                                            └───┘              
src                                           └───┘                
typ                                           └───┘              
doc                                            └───┘
444    {x : zmodp p hp} (hx0 : x ≠ 0) : x.1 ≤ (p / 2 : ℕ) ↔ (p / 2 : ℕ) < (-x).1 :=
id          └───┘  └┘                                         
src         └───┘                                                   
typ         └───┘  └┘                                         
445  @zmod.le_div_two_iff_lt_neg ⟨p, hp.pos⟩ hp1 _ hx0
id    └────────────────────────┘    └┘└──┘  └─┘   └─┘
src   └────────────────────────┘       └──┘
typ   └────────────────────────┘    └┘└──┘  └─┘   └─┘
446  
447  lemma ne_neg_self (hp1 : p % 2 = 1) {a : zmodp p hp} (ha : a ≠ 0) : a ≠ -a :=
id                                         └───┘  └┘                 
src                                         └───┘                        
typ                                        └───┘  └┘                 
448  @zmod.ne_neg_self ⟨p, hp.pos⟩ hp1 _ ha
id    └──────────────┘    └┘└──┘  └─┘   └┘
src   └──────────────┘       └──┘
typ   └──────────────┘    └┘└──┘  └─┘   └┘
449  
450  variable {hp}
451  
452  /-- `val_min_abs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
453    The result will be in the interval `(-n/2, n/2]` -/
454  def val_min_abs (x : zmodp p hp) : ℤ := zmod.val_min_abs x
id                        └───┘  └┘        └──────────────┘ 
src                       └───┘             └──────────────┘
typ                       └───┘  └┘        └──────────────┘ 
doc                                          └──────────────┘
455  
456  @[simp] lemma coe_val_min_abs (x : zmodp p hp) :
id                                      └───┘  └┘
src                                     └───┘
typ                                     └───┘  └┘
doc    └──┘
457    (x.val_min_abs : zmodp p hp) = x :=
id      └──────────┘   └───┘  └┘   
src      └──────────┘   └───┘       
typ     └──────────┘   └───┘  └┘   
doc      └──────────┘
458  zmod.coe_val_min_abs x
id   └──────────────────┘ 
src  └──────────────────┘
typ  └──────────────────┘ 
459  
460  lemma nat_abs_val_min_abs_le (x : zmodp p hp) : x.val_min_abs.nat_abs ≤ p / 2 :=
id                                     └───┘  └┘    └──────────┘└──────┘   
src                                    └───┘          └──────────┘└──────┘    
typ                                    └───┘  └┘    └──────────┘└──────┘   
doc                                                   └──────────┘
461  zmod.nat_abs_val_min_abs_le x
id   └─────────────────────────┘ 
src  └─────────────────────────┘
typ  └─────────────────────────┘ 
462  
463  @[simp] lemma val_min_abs_zero : (0 : zmodp p hp).val_min_abs = 0 :=
id                                         └───┘  └┘ └─────────┘  
src                                        └───┘      └─────────┘  
typ                                        └───┘  └┘ └─────────┘  
doc    └──┘                                           └─────────┘
464  zmod.val_min_abs_zero
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
465  
466  @[simp] lemma val_min_abs_eq_zero (x : zmodp p hp) : x.val_min_abs = 0 ↔ x = 0 :=
id                                          └───┘  └┘    └──────────┘      
src                                         └───┘          └──────────┘       
typ                                         └───┘  └┘    └──────────┘      
doc    └──┘                                                └──────────┘
467  zmod.val_min_abs_eq_zero x
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
468  
469  lemma cast_nat_abs_val_min_abs (a : zmodp p hp) :
id                                       └───┘  └┘
src                                      └───┘
typ                                      └───┘  └┘
470    (a.val_min_abs.nat_abs : zmodp p hp) = if a.val ≤ p / 2 then a else -a :=
id      └──────────┘└──────┘   └───┘  └┘      └──┘                 
src      └──────────┘└──────┘   └───┘            └──┘                   
typ     └──────────┘└──────┘   └───┘  └┘      └──┘                 
doc      └──────────┘
471  zmod.cast_nat_abs_val_min_abs a
id   └───────────────────────────┘ 
src  └───────────────────────────┘
typ  └───────────────────────────┘ 
472  
473  @[simp] lemma nat_abs_val_min_abs_neg (a : zmodp p hp) :
id                                              └───┘  └┘
src                                             └───┘
typ                                             └───┘  └┘
doc    └──┘
474    (-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs :=
id       └─────────┘ └─────┘   └──────────┘└──────┘
src       └─────────┘ └─────┘    └──────────┘└──────┘
typ      └─────────┘ └─────┘   └──────────┘└──────┘
doc        └─────────┘             └──────────┘
475  zmod.nat_abs_val_min_abs_neg _
id   └──────────────────────────┘
src  └──────────────────────────┘
typ  └──────────────────────────┘
476  
477  lemma val_eq_ite_val_min_abs (a : zmodp p hp) :
id                                     └───┘  └┘
src                                    └───┘
typ                                    └───┘  └┘
478    (a.val : ℤ) = a.val_min_abs + if a.val ≤ p / 2 then 0 else p :=
id      └──┘      └──────────┘     └──┘                  
src      └──┘       └──────────┘      └──┘    
typ     └──┘      └──────────┘     └──┘                  
doc                   └──────────┘
479  zmod.val_eq_ite_val_min_abs _
id   └─────────────────────────┘
src  └─────────────────────────┘
typ  └─────────────────────────┘
480  
481  variable (hp)
482  
483  lemma prime_ne_zero {q : ℕ} (hq : prime q) (hpq : p ≠ q) : (q : zmodp p hp) ≠ 0 :=
id                                    └───┘                    └───┘  └┘  
src                                   └───┘                        └───┘       
typ                                   └───┘                    └───┘  └┘  
doc                                    └───┘
484  by rwa [← nat.cast_zero, ne.def, zmodp.eq_iff_modeq_nat, nat.modeq.modeq_zero_iff,
id             └───────────┘  └────┘  └────────────────────┘  └──────────────────────┘
src     └─────┘└───────────┘└┘└────┘└┘└────────────────────┘└┘└──────────────────────┘└─
typ     └─────┘└───────────┘└┘└────┘└┘└────────────────────┘└┘└──────────────────────┘└─
doc     └─────┘             └┘      └┘                      └┘                        └─
txt     └─────┘             └┘      └┘                      └┘                        └─
par     └─────┘             └┘      └┘                      └┘                        └─
pid        └──┘             └┘      └┘                      └┘                        └─
st     └───────────────────┘└──────┘└──────────────────────┘└────────────────────────┘└─
485    ← hp.coprime_iff_not_dvd, coprime_primes hp hq]
id                               └────────────┘ └┘ └┘
src  ───┘                      └┘└────────────┘    └─
typ  ───┘└────────────────────┘└┘└────────────┘└┘└┘└─
doc  ───┘                      └┘                  └─
txt  ───┘                      └┘                  └─
par  ───┘                      └┘                  └─
pid  ───┘                      └┘                  
st   ─────────────────────────┘└────────────────────┘
486  
src  
typ  
doc  
txt  
par  
pid  
st   
487  lemma mul_inv_eq_gcd (a : ℕ) : (a : zmodp p hp) * a⁻¹ = nat.gcd a p :=
id                                     └───┘  └┘   └┘  └─────┘  
src                                     └───┘         └┘  └─────┘
typ                                    └───┘  └┘   └┘  └─────┘  
488  by rw [← int.cast_coe_nat (nat.gcd _ _), nat.gcd_comm, nat.gcd_rec, ← (eq_iff_modeq_int _).2 (int.modeq.gcd_a_modeq _ _)];
id            └──────────────┘  └─────┘       └──────────┘  └─────────┘     └──────────────┘       └───────────────────┘
src     └────┘└──────────────┘ └─────┘└─────┘└──────────┘└┘└─────────┘└──┘ └──────────────┘└────┘ └───────────────────┘└────┘
typ     └────┘└──────────────┘ └─────┘└─────┘└──────────┘└┘└─────────┘└──┘ └──────────────┘└────┘ └───────────────────┘└────┘
doc     └────┘                        └─────┘            └┘           └──┘                 └────┘                      └────┘
txt     └────┘                        └─────┘            └┘           └──┘                 └────┘                      └────┘
par     └────┘                        └─────┘            └┘           └──┘                 └────┘                      └────┘
pid       └──┘                        └─────┘            └┘           └──┘                 └────┘                      └────┘
st     └───────────────────────────────────┘└────────────┘└───────────┘└────────────────────────────────────────────────────┘└─
489    simp [has_inv.inv, val_cast_nat]
id                        └──────────┘
src    └────┘           └┘└──────────┘└─
typ    └────┘           └┘└──────────┘└─
doc    └────┘           └┘            └─
txt    └────┘           └┘            └─
par    └────┘           └┘            └─
pid                   └┘            
st   ───────────────────────────────────
490  
src  
typ  
doc  
txt  
par  
pid  
st   
491  private lemma mul_inv_cancel_aux : ∀ a : zmodp p hp, a ≠ 0 → a * a⁻¹ = 1 :=
id                                            └───┘  └┘          └┘ 
src                                           └───┘                  └┘ 
typ                                           └───┘  └┘          └┘ 
492  λ ⟨a, hap⟩ ha0, begin
id             └─┘
typ            └─┘
st                   └─────
493    rw [mk_eq_cast, ne.def, ← @nat.cast_zero (zmodp p hp), eq_iff_modeq_nat, modeq_zero_iff] at ha0,
id         └────────┘  └────┘     └───────────┘  └───┘  └┘   └──────────────┘  └────────────┘
src    └──┘└────────┘└┘└────┘└──┘ └───────────┘ └───┘   └─┘└──────────────┘└┘└────────────┘└──────┘
typ    └──┘└────────┘└┘└────┘└──┘ └───────────┘ └───┘└┘└─┘└──────────────┘└┘└────────────┘└──────┘
doc    └──┘          └┘      └──┘                       └─┘                └┘              └──────┘
txt    └──┘          └┘      └──┘                       └─┘                └┘              └──────┘
par    └──┘          └┘      └──┘                       └─┘                └┘              └──────┘
pid      └┘          └┘      └──┘                       └─┘                └┘              └─────┘
st   ───────────────┘└──────┘└─────────────────────────────┘└────────────────┘└──────────────┘└─────┘└─
494    have : nat.gcd p a = 1 := (prime.coprime_iff_not_dvd hp).2 ha0,
id            └─────┘          └───────────────────────┘ └┘    └─┘
src    └─────┘└─────┘  └────┘ └───────────────────────┘  └──┘
typ    └─────┘└─────┘└────┘ └───────────────────────┘└┘└──┘└─┘
doc    └─────┘          └────┘                            └──┘
txt    └─────┘          └────┘                            └──┘
par    └─────┘          └────┘                            └──┘
pid    └───┘└┘          └───┘                            └──┘
st   ───────────────────────────────────────────────────────────────┘└─
495    rw [mk_eq_cast _ hap, mul_inv_eq_gcd, nat.gcd_comm],
id         └────────┘   └─┘  └────────────┘  └──────────┘
src    └──┘└────────┘└─┘   └┘└────────────┘└┘└──────────┘
typ    └──┘└────────┘└─┘└─┘└┘└────────────┘└┘└──────────┘
doc    └──┘          └─┘   └┘              └┘            
txt    └──┘          └─┘   └┘              └┘            
par    └──┘          └─┘   └┘              └┘            
pid      └┘          └─┘   └┘              └┘            
st   ─────────────────────┘└──────────────┘└────────────┘└──
496    simpa [nat.gcd_comm, this]
id            └──────────┘  └──┘
src    └─────┘└──────────┘└┘    └┘
typ    └─────┘└──────────┘└┘└──┘└┘
doc    └─────┘            └┘    └┘
txt    └─────┘            └┘    └┘
par    └─────┘            └┘    └┘
pid                     └┘    
st   ────────────────────────────┘
497  end
st   └─┘
498  
499  instance : discrete_field (zmodp p hp) :=
id              └────────────┘  └───┘  └┘
src             └────────────┘  └───┘
typ             └────────────┘  └───┘  └┘
500  { zero_ne_one := fin.ne_of_vne $ show 0 ≠ 1 % p,
id                    └───────────┘              
src                   └───────────┘             
typ                   └───────────┘              
501      by rw nat.mod_eq_of_lt hp.one_lt;
id             └──────────────┘ └───────┘
src         └─┘└──────────────┘└───────┘
typ         └─┘└──────────────┘└───────┘
doc         └─┘                
txt         └─┘                
par         └─┘                
pid                           
st         └───────────────────────────────
502        exact zero_ne_one,
id               └─────────┘
src        └────┘└─────────┘
typ        └────┘└─────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────┘
503    mul_inv_cancel := mul_inv_cancel_aux hp,
id                       └────────────────┘ └┘
src                      └────────────────┘
typ                      └────────────────┘ └┘
504    inv_mul_cancel := λ a, by rw mul_comm; exact mul_inv_cancel_aux hp _,
id                                 └──────┘        └────────────────┘ └┘
src                              └─┘└──────┘  └────┘└────────────────┘  └┘
typ                             └─┘└──────┘  └────┘└────────────────┘└┘└┘
doc                              └─┘          └────┘                    └┘
txt                              └─┘          └────┘                    └┘
par                              └─┘          └────┘                    └┘
pid                                                                   └┘
st                              └─────────────────────────────────────────┘
505    has_decidable_eq := by apply_instance,
src                           └────────────┘
typ                           └────────────┘
doc                           └────────────┘
txt                           └────────────┘
par                           └────────────┘
st                           └─────────────┘
506    inv_zero := show (gcd_a 0 p : zmodp p hp) = 0,
id                       └───┘      └───┘  └┘  
src                      └───┘       └───┘       
typ                      └───┘      └───┘  └┘  
doc                      └───┘
507      by unfold gcd_a xgcd xgcd_aux; refl,
src         └────────────────────────┘  └──┘
typ         └────────────────────────┘  └──┘
doc         └────────────────────────┘  └──┘
txt         └────────────────────────┘  └──┘
par         └────────────────────────┘  └──┘
pid               └──────────────────┘
st         └───────────────────────────────┘
508    ..zmodp.comm_ring hp,
id       └─────────────┘ └┘
src      └─────────────┘
typ      └─────────────┘ └┘
509    ..zmodp.has_inv hp }
id       └───────────┘ └┘
src      └───────────┘
typ      └───────────┘ └┘
510  
511  end zmodp